(4steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable l exists
  A:Type, F:(AProp), L:A List. (k:A. Dec(F(k)))  Dec((kL.F(k)))
By: Auto THEN ListInd -2

Generated subgoals:

1 1. A : Type
2. F : AProp
3. A List
4. k:A. Dec(F(k))
  Dec((knil.F(k)))
1 step
2 1. A : Type
2. F : AProp
3. A List
4. k:A. Dec(F(k))
5. u : A
6. v : A List
7. Dec((kv.F(k)))
  Dec((k[u / v].F(k)))
2 steps

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

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