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