proposition: Theorem cong_antisymmetric_same_relation : forall (U:Type) (R R':Relation U), same_relation U R R' -> Antisymmetric U R -> Antisymmetric U R'.
proof: Proof. compute; intros; elim H; intros; clear H; apply (H0 x y (H3 x y H1) (H3 y x H2)). Qed.
imports: Relations_1