`{Funext} (p : Φ = Ψ) : A/Φ = A/Ψ. Proof. by destruct p, (path_ishprop CΦ CΨ). Defined.
Require Import Basics.Notations. Require Import Import algebra_notations ne_list.notations. Import quotient_algebra_notations.