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