proposition: Lemma induced_function2arg_correct: forall (a:A) (b:B), induced_function2arg (quotient_projection R a) (quotient_projection S b) = f a b.
proof: Proof. intros. unfold induced_function2arg. unfold induced_eval. unfold induced2. rewrite induced_function2_correct. rewrite induced_function_correct. unfold eval. unfold induced1. rewrite induced_function_correct. reflexivity. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec