proposition: Theorem makeTrans_makeRefl_comm : forall s s', makeTrans (makeRefl R) s s' <-> makeRefl (makeTrans R) s s'.
proof: Proof. split. { induction 1; repeat match goal with | [ H : makeRefl _ _ _ |- _ ] => inversion H; clear H; subst end; eauto using RRefl, RStep, TStep, TTrans. } { intros. inversion H; clear H; subst; auto. apply TStep. apply RRefl. induction H0; eauto using RStep, TStep, TTrans. } Qed.
imports: Coq.Classes.RelationClasses Coq.Setoids.Setoid