DEFINITION True_rec()
TYPE =
Π
P:
Set
.P
→
True
→
P
BODY =
Show proof