DEFINITION land_ind()
TYPE =
       ∀A:Prop.∀B:Prop.∀P:Prop.(A→B→P)→(land A B)→P
BODY =
        assume A: Prop
        assume B: Prop
        assume P: Prop
        suppose H: A→B→P
        suppose H1: land A B
          by cases on H1 we prove P
             case conj H2:A H3:B ⇒
                the thesis becomes P
                by (H H2 H3)
P
          we proved P
       we proved ∀A:Prop.∀B:Prop.∀P:Prop.(A→B→P)→(land A B)→P