(11steps 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: cons member 1 1

1. T : Type
2. l : T List
3. a : T
4. x : T
5. i : 
6. i = 0
  0<||[a / l]||  x = [a / l][0]  x = a  (i:i<||l|| & x = l[i])


By: Reduce 0 THEN Sel 1 (Analyze 0)


Generated subgoals:

None

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

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