IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable l exists21 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(F(u) (kv.F(k)))
By:
AllHyps (InstHyp [u]) THEN ProveDecidable
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html