proposition: Lemma class_rep_inc : forall (a : E) (r : E2P) (x : E), is_class a r x -> inc (rep x) x.
proof: Proof. ir. unfold is_class in H. xd. unfold rep in |- *. ap choose_pr. nin H0. apply ex_intro with y; au. Qed.
imports: set_theory