DEFINITION land_ind()
TYPE =
       ∀A:Prop.∀B:Prop.∀P:Prop.(A→B→P)→(land A B)→P
BODY =
Show proof