(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
P
:Prop. (
P
)
P
By:
(Analyze 0) THEN (Unfold `prop_to_bool` 0)
Generated subgoal:
1
1.
P
: Prop
InjCase(lem(
P
) ; true
; false
)
P
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
hol
Sections
HOLlib
Doc