strict
Creates a strict unification strategy, with the given starting context, that checks Terms' equality through plain Term.equals — including for numeric terms, so e.g. an integer 1 and a real 1.0 are not considered equal (unlike with naive).
Creates a strict unification strategy (see strict) with an empty starting context.