proposition: Lemma class_of_eq_class : forall (a : E) (r : E2P) (x : E), inc x a -> class_of a r x = class_in (quotient a r) x.
proof: Proof. ir. ap class_eq_class_of. assert (inc (class_in (quotient a r) x) (quotient a r)). unfold class_in in |- *. assert (ex (fun y : E => A (inc y (quotient a r)) (inc x y))). apply ex_intro with (class_of a r x). xd. ap class_of_in_quotient; au. ap class_of_origin; au. chpr H0. xd. unfold quotient in H0. zpr H0. am. assert (ex (fun y : E => A (inc y (quotient a r)) (inc x y))). apply ex_intro with (class_of a r x). xd. ap class_of_in_quotient; au. ap class_of_origin; au. chpr H0. xd. Qed.
imports: set_theory