DEFINITION land_rec()
TYPE =
       ΠA:Prop
         .ΠB:Prop.ΠP:Set.(A→B→P)→(land A B)→P
BODY =
λA:Prop
         .λB:Prop
           .λP:Set
             .λf:A→B→P.λH:land A B.<λH1:land A B.P> CASE H OF conj H1 H2⇒f H1 H2