DEFINITION True_rec()
TYPE =
       ΠP:Set.P→True→P
BODY =
λP:Set.λp:P.λH:True.<λH1:True.P> CASE H OF I⇒p