is mentioned by

Thm* mt(nil) = True  Prop{1} Thm* & ('a:Type{i}, x:'a, l:'a List. mt(cons(x; l)) = False  Prop{1})	[mt_def]
Thm* 'a:Type{i}, l:'a List. mt(l)  Prop{1}	[mt_wf]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 hol hol prim rec

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html