IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable l all1 1. A : Type
2. F : AProp
3. A List
4. k:A. Dec(F(k))
Dec((knil.F(k)))
By:
Unfold `decidable` 0 THEN OrLeft THEN Easy
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html