actualize set-union with nat by morphism :elem → nat; :set → natset; ∅ → ∅; ++ → ++; # → #; } → }; ∪ → ∪; ∩ → ∩; \ → \; -- → --; ∈ → ∈; ⊆ → ⊆; a → n2; b → n3; c → n4; s → S; s0 → S0; s1 → S1; s2 → S2 end actualize