Def mt(l) == Case of l; nil  True ; a.as'  False

is mentioned by

Thm* 'a:S, l:'a List. mt(l)  hd(l) = head(l)	[hhd_nuprl]
Thm* l:'a List. Dec(mt(l))	[decidable__mt]
Thm* it_sum(nil) = 0 Thm* & (l: List. mt(l)  it_sum(l) = head(l)+it_sum(tl(l))) Thm* & (x:, l: List. it_sum(cons(x; l)) = x+it_sum(l))	[it_sum_def]
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* l:'a List. null(l)  mt(l)	[assert_of_null_is_mt]
Thm* 'a:Type, l:'a List. mt(l)  head(l)  'a	[head_wf]
Thm* l,ll:'a List. mt(l @ ll)  mt(l) & mt(ll)	[mt_append]

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