(6steps 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
2
char
1
1.
P
: Prop
(
P
)
P
By:
Unab [`prop_to_bool_2`]
Generated subgoal:
1
InjCase(lem_2(
P
) ; true
; false
)
P
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc