napply H.
nqed.
+nlemma symmetric_or2 : ∀P1,P2.Or2 P1 P2 → Or2 P2 P1.
+ #P1; #P2; #H;
+ napply (or2_elim P1 P2 ? H);
+ ##[ ##1: #H1; napply (or2_intro2 P2 P1 H1)
+ ##| ##2: #H1; napply (or2_intro1 P2 P1 H1)
+ ##]
+nqed.
+
ninductive Or3 (A,B,C:Prop) : Prop ≝
or3_intro1 : A → (Or3 A B C)
| or3_intro2 : B → (Or3 A B C)
napply H.
nqed.
+nlemma symmetric_or3_12 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P2 P1 P3.
+ #P1; #P2; #P3; #H;
+ napply (or3_elim P1 P2 P3 ? H);
+ ##[ ##1: #H1; napply (or3_intro2 P2 P1 P3 H1)
+ ##| ##2: #H1; napply (or3_intro1 P2 P1 P3 H1)
+ ##| ##3: #H1; napply (or3_intro3 P2 P1 P3 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or3_13 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P3 P2 P1.
+ #P1; #P2; #P3; #H;
+ napply (or3_elim P1 P2 P3 ? H);
+ ##[ ##1: #H1; napply (or3_intro3 P3 P2 P1 H1)
+ ##| ##2: #H1; napply (or3_intro2 P3 P2 P1 H1)
+ ##| ##3: #H1; napply (or3_intro1 P3 P2 P1 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or3_23 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P1 P3 P2.
+ #P1; #P2; #P3; #H;
+ napply (or3_elim P1 P2 P3 ? H);
+ ##[ ##1: #H1; napply (or3_intro1 P1 P3 P2 H1)
+ ##| ##2: #H1; napply (or3_intro3 P1 P3 P2 H1)
+ ##| ##3: #H1; napply (or3_intro2 P1 P3 P2 H1)
+ ##]
+nqed.
+
ninductive Or4 (A,B,C,D:Prop) : Prop ≝
or4_intro1 : A → (Or4 A B C D)
| or4_intro2 : B → (Or4 A B C D)
napply H.
nqed.
+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)
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.
+
ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
ex_intro: ∀x:A.Q x → ex A Q.