Sound behavioral equations on open terms may become unsound after
conservative extensions of the underlying operational semantics. Providing
criteria under which such equations are preserved is extremely useful; in
particular, it can avoid the need to repeat proofs when extending the specified
language.