(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. T : Type
2. l : T List
3. a : T
4. x : T
5. i:. i<||[a / l]|| & x = [a / l][i]
  x = a  (i:. i<||l|| & x = l[i])
By: ExRepD THEN MoveToConcl -1 THEN MoveToConcl -1 THEN CaseNatZero `i'

Generated subgoals:

1 5. i : 
6. i = 0
  0<||[a / l]||  x = [a / l][0]  x = a  (i:. i<||l|| & x = l[i])
1 step
2 5. i : 
6. i  0
7. 0<i
  i<||[a / l]||  x = [a / l][i]  x = a  (i:. i<||l|| & x = l[i])
3 steps

About:
listconsnatural_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