DEFINITION B_rec()
TYPE =
       ΠP:B→Set
         .(P Abbr)→(P Abst)→(P Void)→Πb:B.(P b)
BODY =
λP:B→Set
         .λp:P Abbr.λp1:P Abst.λp2:P Void.λb:B.<P> CASE b OF Abbr⇒p | Abst⇒p1 | Void⇒p2