% Imports List.thmod twice, at nat and bool, showing quoted file
% imports with aliases and positional type arguments.
Kind nat type.
Kind bool type.
Type z nat.
Type s nat -> nat.
Type t bool.
Type f bool.
Import Module N = "List"[nat].
Import Module B = "List"[bool].
Theorem nat_ok : forall (xs:N.lst), N.contains z xs -> N.contains z xs.
intros. search.
Theorem bool_ok : forall (xs:B.lst), B.contains t xs -> B.contains t xs.
intros. search.
