specification
using rename
wellfounded
by morphism
:Elem → Elem1;
≪ → ≪1;
end rename, rename
wellfounded
by morphism
:Elem → Elem2;
≪ → ≪2;
end rename
end specification