fact: Fixpoint leftTrans_makeTrans_acc x y (l : leftTrans x y) : makeTrans x y := match l with | LTFin pf => TStep pf | LTStep _ pf pfL => TTrans (TStep pf) (leftTrans_makeTrans_acc pfL) end.
imports: Coq.Classes.RelationClasses Coq.Setoids.Setoid