proposition: Theorem cong_transitive_same_relation : forall (U:Type) (R R':Relation U), same_relation U R R' -> Transitive U R -> Transitive U R'.
proof: Proof. intros U R R' H' H'0; red. elim H'. intros H'1 H'2 x y z H'3 H'4; apply H'2. apply H'0 with y; auto with sets. Qed.
imports: Relations_1