% Imports Box.thmod at two element types. The two instances have
% distinct internal box types, while parameter occurrences are replaced
% by the supplied arguments.
Module BoxUse.
Kind u type.
Kind v type.
Import Module B1 = "Box"[u].
Import Module B2 = "Box"[v].
Type f B1.box -> prop.
Type g B2.box -> prop.
End BoxUse.
