proposition: Theorem makeTrans_idem : forall s s', makeTrans (makeTrans R) s s' <-> makeTrans R s s'.
proof: Proof. split. { induction 1; eauto using TTrans. } { eapply TStep. } Qed.
imports: Coq.Classes.RelationClasses Coq.Setoids.Setoid