(3steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prop
to
bool
char
1
1.
P
: Prop
InjCase(lem(
P
) ; true
; false
)
P
By:
GenDC (lem(
P
)) THEN StrongAuto
Generated subgoal:
1
2.
P
Void
3.
P
False
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc