Definitions
bool
1
Doc
At:
ifthenelse
wf
1
1.
b:
2.
A:
Type
3.
p:
A
4.
q:
A
if b
p else q fi
A
By:
Unfold `ifthenelse` 0
THEN
Unfold `bool` 1
Generated subgoal:
1
1.
b:
Unit+Unit
2.
A:
Type
3.
p:
A
4.
q:
A
dec(b ; p; q)
A