This doesn't type check properly in the old MathExpTypeResolver, so it would be a good test for the new type system.
Enhancement Merge_Store_Capability for Search_Store_Template;
Operation Merge (updates S: Store; clears T: Store);
requires ||S|| + ||T|| <= Max_Capacity;
ensures for all k: Key, S(k) iff #S(k) or #T(k);
end Merge_Store_Capability