proposition: Lemma equivalent_trans : forall (a : E) (r : E2P) (x y z : E), equivalent a r x y -> equivalent a r y z -> equivalent a r x z.
proof: Proof. unfold equivalent in |- *; ir; xd. transitivity (class_of a r y); au. Qed.
imports: set_theory