-(* if are_invertible maxvar vl l r then
- (prerr_endline ("Invertible " ^ (Pp.pp_foterm l) ^ "=" ^
- (Pp.pp_foterm r));
- DT.index t l (Terms.Left2Right, c))
- else *)
- DT.index
- (DT.index t l (Terms.Left2Right, c))
- r (Terms.Right2Left, c)
+ op (op t l (Terms.Left2Right, c))
+ r (Terms.Right2Left, c)
+ | (_,Terms.Equation (l,r,_,Terms.Invertible),vl,_) as c ->
+ op t l (Terms.Left2Right, c)