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