let is_identity_clause ~unify = function
| _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
| _, Terms.Equation (l,r,_,_), vl, proof when unify ->
let is_identity_clause ~unify = function
| _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
| _, Terms.Equation (l,r,_,_), vl, proof when unify ->