proposition: Lemma induced_function3_correct: forall (a:A) (b:B), induced_function3 (quotient_projection R a) (quotient_projection S b) = quotient_projection T (f a b).
proof: Proof. intros. unfold induced_function3. rewrite induced_function2arg_correct. reflexivity. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec