merge
open override fun merge(substitution1: Substitution, substitution2: Substitution, occurCheckEnabled: Boolean): Substitution
When occurCheckEnabled is false, this first attempts a quick Substitution.plus-based union of context, substitution1 and substitution2; only if that union is contradictory does it fall back to the full, equation-based merge (which also re-unifies, rather than merely composes, bindings shared by both operands).