DEFINITION land_rect()
TYPE =
       ΠA:Prop
         .ΠB:Prop
           .ΠP:(Type:785:cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/land_rect.con)
             .(A→B→P)→(land A B)→P
BODY =
Show proof