+nlemma symmetric_or4_12 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P2 P1 P3 P4.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro2 P2 P1 P3 P4 H1)
+ ##| ##2: #H1; napply (or4_intro1 P2 P1 P3 P4 H1)
+ ##| ##3: #H1; napply (or4_intro3 P2 P1 P3 P4 H1)
+ ##| ##4: #H1; napply (or4_intro4 P2 P1 P3 P4 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_13 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P3 P2 P1 P4.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro3 P3 P2 P1 P4 H1)
+ ##| ##2: #H1; napply (or4_intro2 P3 P2 P1 P4 H1)
+ ##| ##3: #H1; napply (or4_intro1 P3 P2 P1 P4 H1)
+ ##| ##4: #H1; napply (or4_intro4 P3 P2 P1 P4 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_14 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P4 P2 P3 P1.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro4 P4 P2 P3 P1 H1)
+ ##| ##2: #H1; napply (or4_intro2 P4 P2 P3 P1 H1)
+ ##| ##3: #H1; napply (or4_intro3 P4 P2 P3 P1 H1)
+ ##| ##4: #H1; napply (or4_intro1 P4 P2 P3 P1 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_23 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P3 P2 P4.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro1 P1 P3 P2 P4 H1)
+ ##| ##2: #H1; napply (or4_intro3 P1 P3 P2 P4 H1)
+ ##| ##3: #H1; napply (or4_intro2 P1 P3 P2 P4 H1)
+ ##| ##4: #H1; napply (or4_intro4 P1 P3 P2 P4 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_24 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P4 P3 P2.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro1 P1 P4 P3 P2 H1)
+ ##| ##2: #H1; napply (or4_intro4 P1 P4 P3 P2 H1)
+ ##| ##3: #H1; napply (or4_intro3 P1 P4 P3 P2 H1)
+ ##| ##4: #H1; napply (or4_intro2 P1 P4 P3 P2 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_34 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P2 P4 P3.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro1 P1 P2 P4 P3 H1)
+ ##| ##2: #H1; napply (or4_intro2 P1 P2 P4 P3 H1)
+ ##| ##3: #H1; napply (or4_intro4 P1 P2 P4 P3 H1)
+ ##| ##4: #H1; napply (or4_intro3 P1 P2 P4 P3 H1)
+ ##]
+nqed.
+
+ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
+ or5_intro1 : A → (Or5 A B C D E)
+| or5_intro2 : B → (Or5 A B C D E)
+| or5_intro3 : C → (Or5 A B C D E)
+| or5_intro4 : D → (Or5 A B C D E)
+| or5_intro5 : E → (Or5 A B C D E).
+
+nlemma or5_elim
+ : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q.
+ ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q.
+ #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5;
+ napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?);
+ napply H.
+nqed.
+
+nlemma symmetric_or5_12 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P2 P1 P3 P4 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro2 P2 P1 P3 P4 P5 H1)
+ ##| ##2: #H1; napply (or5_intro1 P2 P1 P3 P4 P5 H1)
+ ##| ##3: #H1; napply (or5_intro3 P2 P1 P3 P4 P5 H1)
+ ##| ##4: #H1; napply (or5_intro4 P2 P1 P3 P4 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P2 P1 P3 P4 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_13 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P3 P2 P1 P4 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro3 P3 P2 P1 P4 P5 H1)
+ ##| ##2: #H1; napply (or5_intro2 P3 P2 P1 P4 P5 H1)
+ ##| ##3: #H1; napply (or5_intro1 P3 P2 P1 P4 P5 H1)
+ ##| ##4: #H1; napply (or5_intro4 P3 P2 P1 P4 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P3 P2 P1 P4 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_14 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P4 P2 P3 P1 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro4 P4 P2 P3 P1 P5 H1)
+ ##| ##2: #H1; napply (or5_intro2 P4 P2 P3 P1 P5 H1)
+ ##| ##3: #H1; napply (or5_intro3 P4 P2 P3 P1 P5 H1)
+ ##| ##4: #H1; napply (or5_intro1 P4 P2 P3 P1 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P4 P2 P3 P1 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_15 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P5 P2 P3 P4 P1.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro5 P5 P2 P3 P4 P1 H1)
+ ##| ##2: #H1; napply (or5_intro2 P5 P2 P3 P4 P1 H1)
+ ##| ##3: #H1; napply (or5_intro3 P5 P2 P3 P4 P1 H1)
+ ##| ##4: #H1; napply (or5_intro4 P5 P2 P3 P4 P1 H1)
+ ##| ##5: #H1; napply (or5_intro1 P5 P2 P3 P4 P1 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_23 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P3 P2 P4 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P3 P2 P4 P5 H1)
+ ##| ##2: #H1; napply (or5_intro3 P1 P3 P2 P4 P5 H1)
+ ##| ##3: #H1; napply (or5_intro2 P1 P3 P2 P4 P5 H1)
+ ##| ##4: #H1; napply (or5_intro4 P1 P3 P2 P4 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P1 P3 P2 P4 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_24 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P4 P3 P2 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P4 P3 P2 P5 H1)
+ ##| ##2: #H1; napply (or5_intro4 P1 P4 P3 P2 P5 H1)
+ ##| ##3: #H1; napply (or5_intro3 P1 P4 P3 P2 P5 H1)
+ ##| ##4: #H1; napply (or5_intro2 P1 P4 P3 P2 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P1 P4 P3 P2 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_25 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P5 P3 P4 P2.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P5 P3 P4 P2 H1)
+ ##| ##2: #H1; napply (or5_intro5 P1 P5 P3 P4 P2 H1)
+ ##| ##3: #H1; napply (or5_intro3 P1 P5 P3 P4 P2 H1)
+ ##| ##4: #H1; napply (or5_intro4 P1 P5 P3 P4 P2 H1)
+ ##| ##5: #H1; napply (or5_intro2 P1 P5 P3 P4 P2 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_34 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P4 P3 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P2 P4 P3 P5 H1)
+ ##| ##2: #H1; napply (or5_intro2 P1 P2 P4 P3 P5 H1)
+ ##| ##3: #H1; napply (or5_intro4 P1 P2 P4 P3 P5 H1)
+ ##| ##4: #H1; napply (or5_intro3 P1 P2 P4 P3 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P1 P2 P4 P3 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_35 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P5 P4 P3.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P2 P5 P4 P3 H1)
+ ##| ##2: #H1; napply (or5_intro2 P1 P2 P5 P4 P3 H1)
+ ##| ##3: #H1; napply (or5_intro5 P1 P2 P5 P4 P3 H1)
+ ##| ##4: #H1; napply (or5_intro4 P1 P2 P5 P4 P3 H1)
+ ##| ##5: #H1; napply (or5_intro3 P1 P2 P5 P4 P3 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_45 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P3 P5 P4.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P2 P3 P5 P4 H1)
+ ##| ##2: #H1; napply (or5_intro2 P1 P2 P3 P5 P4 H1)
+ ##| ##3: #H1; napply (or5_intro3 P1 P2 P3 P5 P4 H1)
+ ##| ##4: #H1; napply (or5_intro5 P1 P2 P3 P5 P4 H1)
+ ##| ##5: #H1; napply (or5_intro4 P1 P2 P3 P5 P4 H1)
+ ##]
+nqed.
+