raise (UnificationFailure (lazy "Inference.unification.unif"))
| Terms.Var i, t -> Subst.build_subst i t subst
| t, Terms.Var i when occurs_check subst i t ->
raise (UnificationFailure (lazy "Inference.unification.unif"))
raise (UnificationFailure (lazy "Inference.unification.unif"))
| Terms.Var i, t -> Subst.build_subst i t subst
| t, Terms.Var i when occurs_check subst i t ->
raise (UnificationFailure (lazy "Inference.unification.unif"))