Some dualization clean-up.

[helm.git] / helm / software / matita / contribs / ng_assembly / common / theory.ma

diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index 7f5f9003658d6d621d2b8240357f4ada4565a1a0..bab796daa3b732a1714d2a50909eba646dc263aa 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -16,11 +16,14 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
 universe constraint Type[0] < Type[1].
+universe constraint Type[1] < Type[2].
+universe constraint Type[2] < Type[3].
+universe constraint Type[3] < Type[4].
 
 (* ********************************** *)
 (* SOTTOINSIEME MINIMALE DELLA TEORIA *)
@@ -42,7 +45,7 @@ nlemma absurd : ∀A,C:Prop.A → ¬A → C.
  #A; #C; #H;
  nnormalize;
  #H1;
- nelim (H1 H);
+ nelim (H1 H).
 nqed.
 
 nlemma not_to_not : ∀A,B:Prop. (A → B) → ((¬B) → (¬A)).
@@ -175,7 +178,7 @@ ninductive Or2 (A,B:Prop) : Prop ≝
 
 interpretation "logical or" 'or x y = (Or2 x y).
 
-ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
+ndefinition decidable ≝ λA:Prop.A ∨ (¬A).
 
 nlemma or2_elim
  : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
@@ -184,6 +187,14 @@ nlemma or2_elim
  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)
@@ -196,6 +207,33 @@ nlemma or3_elim
  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)
@@ -210,6 +248,66 @@ nlemma or4_elim
  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)
@@ -225,6 +323,116 @@ nlemma or5_elim
  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.
 
@@ -233,13 +441,10 @@ interpretation "exists" 'exists x = (ex ? x).
 ninductive ex2 (A:Type) (Q,R:A → Prop) : Prop ≝
  ex_intro2: ∀x:A.Q x → R x → ex2 A Q R.
 
-ndefinition iff ≝
-λA,B.(A → B) ∧ (B → A).
-
 (* higher_order_defs/relations *)
 
 ndefinition relation : Type → Type ≝
-λA:Type.A → A → Prop. 
+λA.A → A → Prop. 
 
 ndefinition reflexive : ∀A:Type.∀R:relation A.Prop ≝
 λA.λR.∀x:A.R x x.
@@ -267,6 +472,8 @@ ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
 ninductive eq (A:Type) (x:A) : A → Prop ≝
  refl_eq : eq A x x.
 
+ndefinition refl ≝ refl_eq.
+
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
@@ -298,13 +505,93 @@ nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  napply refl_eq.
 nqed.
 
-nlemma eq_elim_r: ∀A:Type.∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
+nlemma eq_ind_r: ∀A:Type[0].∀x:A.∀P:A → Prop.P x → ∀y:A.y=x → P y.
  #A; #x; #P; #H; #y; #H1;
  nrewrite < (symmetric_eq … H1);
  napply H.
 nqed.
 
-nlemma symmetric_neq : ∀T.∀x,y:T.x ≠ y → y ≠ x.
+ndefinition R0 ≝ λT:Type[0].λt:T.t.
+
+ndefinition R1 ≝ eq_rect_Type0.
+
+ndefinition R2 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type[0].
+  ∀a1:T1 a0 (refl_eq ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+  ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
+  ∀b0:T0.
+  ∀e0:a0 = b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:R1 ?? T1 a1 ? e0 = b1.
+  T2 b0 e0 b1 e1.
+ #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
+ napply (eq_rect_Type0 ????? e1);
+ napply (R1 ?? ? ?? e0);
+ napply a2;
+nqed.
+
+ndefinition R3 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. a0=x0 → Type[0].
+  ∀a1:T1 a0 (refl_eq ? a0).
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+  ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
+  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
+      ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
+  ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).
+  ∀b0:T0.
+  ∀e0:a0 = b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:R1 ?? T1 a1 ? e0 = b1.
+  ∀b2: T2 b0 e0 b1 e1.
+  ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
+  T3 b0 e0 b1 e1 b2 e2.
+ #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
+ napply (eq_rect_Type0 ????? e2);
+ napply (R2 ?? ? ???? e0 ? e1);
+ napply a3;
+nqed.
+
+ndefinition R4 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
+  ∀a1:T1 a0 (refl_eq T0 a0).
+  ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
+  ∀a2:T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1).
+  ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+      ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
+  ∀a3:T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1) 
+      a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2). 
+  ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+      ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+      ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. 
+      Type[0].
+  ∀a4:T4 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1) 
+      a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2) 
+      a3 (refl_eq (T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1) 
+                   a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2))
+                   a3).
+  ∀b0:T0.
+  ∀e0:eq (T0 …) a0 b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
+  ∀b2: T2 b0 e0 b1 e1.
+  ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
+  ∀b3: T3 b0 e0 b1 e1 b2 e2.
+  ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
+  T4 b0 e0 b1 e1 b2 e2 b3 e3.
+ #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
+ napply (eq_rect_Type0 ????? e3);
+ napply (R3 ????????? e0 ? e1 ? e2);
+ napply a4;
+nqed.
+
+nlemma symmetric_neq : ∀T:Type.∀x,y:T.x ≠ y → y ≠ x.
  #T; #x; #y;
  nnormalize;
  #H; #H1;