proposition: Lemma well_defined_induced1: forall a1 a2:A, R a1 a2 -> eq_fn (induced1 a1) (induced1 a2).
proof: Proof. unfold eq_fn. intros. pose proof (quotient_projection_surjective b). destruct H0. rewrite <- H0. unfold induced1. unfold quotient_projection. rewrite !induced_function_correct. apply well_defined_2arg. - assumption. - apply (equiv_refl equivS). Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(ImageImplicit) ZornsLemma(Relation_Definitions_Implicit) Coq(Description) Coq(ProofIrrelevance)