DEFINITION bool_rec()
TYPE =
       ΠP:bool→Set
         .(P true)→(P false)→Πb:bool.(P b)
BODY =
λP:bool→Set.λp:P true.λp1:P false.λb:bool.<P> CASE b OF true⇒p | false⇒p1