DEFINITION B_ind()
TYPE =
∀
P:
B
→
Prop
.(P
Abbr
)
→
(P
Abst
)
→
(P
Void
)
→
∀
b:
B
.(P b)
BODY =
Show proof