DEFINITION B_rec()
TYPE =
Π
P:
B
→
Set
.(P
Abbr
)
→
(P
Abst
)
→
(P
Void
)
→
Π
b:
B
.(P b)
BODY =
Show proof