% A parameterized list theory with an internal lst Kind, constructors,
% a declared predicate, and an axiom. It is imported at two element
% types by ListUse.thm.
Module List[T].
Kind lst type.
Type lnil lst.
Type lcons T -> lst -> lst.
Type contains T -> lst -> prop.
Axiom head : forall (x:T) (xs:lst), contains x (lcons x xs).
End List.
