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