Definitions
bool
1
Doc
At:
bool
ind
P:(
Prop). P(false
)
P(true
)
{
b:
. P(b)}
By:
Unfold `guard` 0
THEN
UnivCD
Generated subgoal:
1
1.
P:
Prop
2.
P(false
)
3.
P(true
)
4.
b:
P(b)