proposition: Corollary id_first_isomorphism_surjection : (A / cong_ker f) = B.
proof: Proof. exact (id_isomorphic isomorphic_first_isomorphism_surjection). Qed.
imports: HSet Colimits.Quotient Modalities.ReflectiveSubuniverse Classes.interfaces.canonical_names Classes.theory.ua_isomorphic Classes.theory.ua_subalgebra Classes.theory.ua_quotient_algebra