proposition: Lemma class_of_rep : forall (a : E) (r : E2P) (x : E), inc x (quotient a r) -> class_of a r (rep x) = x.
proof: Proof. ir. ap class_eq_class_of. ap in_quotient_is_class; au. assert (is_class a r x). ap in_quotient_is_class; au. unfold is_class in H0; xd. unfold rep in |- *. nin H1. ap choose_pr. apply ex_intro with y. am. Qed.
imports: set_theory