DEFINITION bool_rec()
TYPE =
Π
P:
bool
→
Set
.(P
true
)
→
(P
false
)
→
Π
b:
bool
.(P b)
BODY =
Show proof