proposition: Lemma well_defined_induced1: forall a1 a2:A, R a1 a2 -> eq_fn (induced1 a1) (induced1 a2).
proof: Proof. unfold eq_fn. intros. pose proof (quotient_projection_surjective b). destruct H0. rewrite <- H0. unfold induced1. rewrite induced_function_correct. rewrite induced_function_correct. apply well_defined_2arg. assumption. apply (equiv_refl equivS). Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec