proposition: Lemma description_of_fbar: forall xbar:quotient R, exists! y:B, exists x:A, quotient_projection R x = xbar /\ f x = y.
proof: Proof. intro. pose proof (quotient_projection_surjective xbar). destruct H. exists (f x). unfold unique. split. exists x. tauto. intros. destruct H0. destruct H0. rewrite <- H1. apply well_defined. apply equality_of_equiv_class_impl_R; trivial. transitivity (proj1_sig (quotient_projection R x)). trivial. rewrite H. rewrite <- H0. trivial. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec