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