IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable mt11 1. 'a : Type
2. l : 'a List
(Case of l; nil True ; a.as' False)
(Case of l; nil True ; a.as' False)
By:
Last ListInd THEN Reduce 0 THEN Simpsetp [`nlogic`]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(Case of l; nil 
True ; a.as' 
(Case of l; nil 
