(2steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: null member
  T:Type, L:T List, x:T. null(L)  (x  L)
By: RW assert_pushdownC 0 THEN HypSubst -1 0

Generated subgoal:

1 1. T : Type
2. L : T List
3. x : T
4. L = nil
  (x  nil)
1 step

About:
listnilassertuniverseimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(2steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc