DEFINITION or3_ind()
TYPE =
       ∀P0:Prop
         .∀P1:Prop.∀P2:Prop.∀P:Prop.(P0→P)→(P1→P)→(P2→P)→(or3 P0 P1 P2)→P
BODY =
        assume P0: Prop
        assume P1: Prop
        assume P2: Prop
        assume P: Prop
        suppose H: P0→P
        suppose H1: P1→P
        suppose H2: P2→P
        suppose H3: or3 P0 P1 P2
          by cases on H3 we prove P
             case or3_intro0 H4:P0 ⇒
                the thesis becomes P
                by (H H4)
P
             case or3_intro1 H4:P1 ⇒
                the thesis becomes P
                by (H1 H4)
P
             case or3_intro2 H4:P2 ⇒
                the thesis becomes P
                by (H2 H4)
P
          we proved P
       we proved 
          ∀P0:Prop
            .∀P1:Prop.∀P2:Prop.∀P:Prop.(P0→P)→(P1→P)→(P2→P)→(or3 P0 P1 P2)→P