Def S == {T:Type| x:T. True }

is mentioned by

Thm* 'a:S, f:('a), x1,x2:'a. f(x1) & f(x2)  x1 = x2

[fun_eq_lemma]

In prior sections: hol hol min hol bool hol prim rec hol arithmetic 2

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