proposition: Lemma equivalent_universal : forall (a : E) (r s : E2P), is_eq_reln a s -> (forall x y : E, inc x a -> inc y a -> r x y -> s x y) -> forall x y : E, equivalent a r x y -> s x y.
proof: Proof. ir. set (z := Z a (fun u : E => s x u)). assert (sub z a). unfold z in |- *; ap Z_sub. unfold sub in H2. unfold equivalent in H1; xd. assert (sub (class_of a r y) z). rewrite <- H4. ap class_of_sub. unfold z in |- *; Ztac. unfold is_eq_reln in H; xd. unfold is_part in |- *; xd. ir. unfold z in |- *; Ztac. unfold is_eq_reln in H; xd. apply H9 with x0; au. unfold z in H5; Ztac. ir. unfold z in |- *; Ztac. unfold is_eq_reln in H; xd. apply H9 with x0; au. unfold z in H5; Ztac. assert (inc y z). ap H5; ap class_of_origin. au. unfold z in H6; Ztac. Qed.
imports: set_theory