| _, Terms.Equation (l,r,_,_), vl, proof ->
(try Some (Unif.unification (* vl *) [] l r)
with FoUnif.UnificationFailure _ -> None)
| _, Terms.Equation (l,r,_,_), vl, proof ->
(try Some (Unif.unification (* vl *) [] l r)
with FoUnif.UnificationFailure _ -> None)