| _, [], [Terms.Equation (l,r,_,_),_], vl, proof when unify ->
(try ignore(Unif.unification (* vl *) [] l r); true
with FoUnif.UnificationFailure _ -> false)
| _, [], [Terms.Equation (l,r,_,_),_], vl, proof when unify ->
(try ignore(Unif.unification (* vl *) [] l r); true
with FoUnif.UnificationFailure _ -> false)