fact: Fixpoint leftTrans_trans x y (l : leftTrans x y) : forall z (r : leftTrans y z), leftTrans x z := match l with | LTFin pf => fun _ pfL => LTStep pf pfL | LTStep _ pf pfL => fun _ pfR => LTStep pf (leftTrans_trans pfL pfR) end.
imports: Coq.Classes.RelationClasses Coq.Setoids.Setoid