proposition: Lemma induced_function2_correct: forall a:A, induced_function2 (quotient_projection R a) = quotient_projection S (f a).
proof: Proof. intros. unfold induced_function2. unfold quotient_projection. rewrite induced_function_correct. reflexivity. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(ImageImplicit) ZornsLemma(Relation_Definitions_Implicit) Coq(Description) Coq(ProofIrrelevance)