proposition: Lemma induced_function_correct: forall x:A, induced_function (quotient_projection R x) = f x.
proof: Proof. intro. unfold induced_function. destruct constructive_definite_description. simpl. destruct e. destruct H. rewrite <- H0. apply well_defined. apply quotient_projection_minimally_collapses_R; trivial. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec