mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Dec(P) == P  P

is mentioned by

Thm* x:T, l:T List. (y:T. Dec(x = y))  Dec((x  l))[l_member_decidable]
Thm* L:T List, P:(||L||Prop).
Thm* (x:||L||. Dec(P(x)))
Thm* 
Thm* (i,j:||L||. P(i)  i<j  P(j))
Thm* 
Thm* (L_1,L_2:T List. L = (L_1 @ L_2) & (i:||L||. P(i)  ||L_1||i))		[append_split2]

In prior sections: core int 1 bool 1 int 2 mb basic rel 1 mb nat

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

mb list 1 Sections MarkB generic Doc