proposition: Lemma quotient_projection_surjective: forall xbar:quotient, exists x:A, quotient_projection x = xbar.
proof: Proof. intro. destruct xbar. destruct i. exists x. unfold quotient_projection. pose proof e. symmetry in H; destruct H. f_equal. apply proof_irrelevance. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec