proposition: Theorem makeTrans_leftTrans : forall s s', makeTrans s s' <-> leftTrans s s'.
proof: Proof. split; intros. { induction H. eapply LTFin. eassumption. eapply leftTrans_trans; eassumption. } { apply leftTrans_makeTrans_acc. assumption. } Qed.
imports: Coq.Classes.RelationClasses Coq.Setoids.Setoid