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 =
λA:Prop
         .λB:Prop
           .λP:(Type:785:cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/land_rect.con)
             .λf:A→B→P.λH:land A B.<λH1:land A B.P> CASE H OF conj H1 H2⇒f H1 H2