DEFINITION land_rec()
TYPE =
       ΠA:Prop
         .ΠB:Prop.ΠP:Set.(A→B→P)→(land A B)→P
BODY =
Show proof