proposition: Lemma quotient_projection_collapses_R: forall x1 x2:A, R x1 x2 -> quotient_projection x1 = quotient_projection x2.
proof: Proof. intros. apply subset_eq_compat. apply R_impl_equality_of_equiv_class. assumption. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec