IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prop to bool 2 char112 1. P : Prop
2. v:P+(PVoid). InjCase(v ; true; false) P InjCase(lem_2(P) ; true; false) P
By:
InstHyp [lem_2(P)] 2 THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
v:P+(P
Void). InjCase(v ; true
; false
P
InjCase(lem_2(P) ; true
