proposition: Lemma induced_function2_correct: forall a:A, induced_function2 (quotient_projection R a) = quotient_projection S (f a).
proof: Proof. intros. unfold induced_function2. rewrite induced_function_correct. reflexivity. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec