proposition: Lemma induced_function_correct: forall (x:A) Hx, induced_function (exist _ (equiv_class R x) Hx) = f x.
proof: Proof. intros. unfold induced_function. destruct constructive_definite_description. simpl. destruct e as [x1 []]. subst. apply well_defined. inversion H; subst; clear H. assert (In (equiv_class R x1) x) as []; try assumption. rewrite H1. constructor. apply equiv. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(ImageImplicit) ZornsLemma(Relation_Definitions_Implicit) Coq(Description) Coq(ProofIrrelevance)