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