% Imports Keys.thmod mapping p, then aliases that instance and maps
% the remaining key q. The axiom remains a key in both instances.
Module KeysUse.
Kind u type.
Type r u -> prop.
Import Module K1 = "Keys"[u] with p := r.
Import Module K2 = K1 with q := r.
End KeysUse.
