proposition: Lemma equivalent_to_rep : forall (a : E) (r : E2P) (x : E), inc x a -> equivalent a r x (rep (class_of a r x)).
proof: Proof. ir. unfold equivalent in |- *; xd. assert (sub (class_of a r x) a). ap class_of_sub; au. ap lem1. ap H0. ap nonempty_rep. apply nonempty_intro with x; ap class_of_origin. am. ap intersecting_classes_of_eq. am. assert (sub (class_of a r x) a). set (x_ := lem1); ap class_of_sub; au. ap H0. ap nonempty_rep. apply nonempty_intro with x; ap class_of_origin. am. apply nonempty_intro with (rep (class_of a r x)). ap intersection2_inc. ap nonempty_rep. apply nonempty_intro with x; ap class_of_origin. am. ap class_of_origin. assert (sub (class_of a r x) a). ap class_of_sub. au. ap lem1. ap H0. ap nonempty_rep. apply nonempty_intro with x. ap class_of_origin. am. Qed.
imports: set_theory