proposition: Lemma third_surjecton_well_def (s : Sort σ) (x y : A s) (P : Ψ s x y) : class_of (Φ s) x = class_of (Φ s) y.
proof: Proof. apply qglue. exact (subrel s x y P). Defined.
imports: Colimits.Quotient Classes.interfaces.canonical_names Classes.theory.ua_quotient_algebra Classes.theory.ua_isomorphic Classes.theory.ua_first_isomorphism