proposition: Lemma quotient_projection_minimally_collapses_R: forall x1 x2:A, quotient_projection x1 = quotient_projection x2 -> R x1 x2.
proof: Proof. intros. apply equality_of_equiv_class_impl_R. repeat rewrite <- quotient_projection_correct. rewrite H. reflexivity. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec