| (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c ->
DT.index t r (Terms.Right2Left, c)
| (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c ->
| (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c ->
DT.index t r (Terms.Right2Left, c)
| (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c ->
(prerr_endline ("Invertible " ^ (Pp.pp_foterm l) ^ "=" ^
(Pp.pp_foterm r));
DT.index t l (Terms.Left2Right, c))
(prerr_endline ("Invertible " ^ (Pp.pp_foterm l) ^ "=" ^
(Pp.pp_foterm r));
DT.index t l (Terms.Left2Right, c))