From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 27 Jul 2011 21:25:17 +0000 (+0000)
Subject: - xoa: bug fix and improvement
X-Git-Tag: make_still_working~2348
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f9201115d73cc65ab2aadc1a7c94cd52564d3b2e;p=helm.git

- xoa: bug fix and improvement
- *_defs: optimization
- confluence: case "flat-theta" closed
---

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index 54f9da02a..d2dd9b345 100644
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -10,8 +10,6 @@
       V_______________________________________________________________ *)
 
 include "basics/list.ma".
-include "lambda-delta/xoa_defs.ma".
-include "lambda-delta/xoa_notation.ma".
 
 (* ARITHMETICAL PROPERTIES **************************************************)
 
diff --git a/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma
index 241119108..8adec5ca5 100644
--- a/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma
+++ b/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma
@@ -30,9 +30,9 @@ interpretation
 
 lemma lpr_inv_item1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
                          ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
-#L1 #L2 #H elim H -H L1 L2
+#L1 #L2 * -L1 L2
 [ #K1 #I #V1 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #_ #L #J #W #H destruct - K1 I V1 /2 width=5/
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
 ]
 qed.
 
diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
index 6e632f72d..cb2b7c947 100644
--- a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
+++ b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
@@ -103,7 +103,7 @@ lemma tpr_conf_flat_theta:
    V0 ⇒ V1 → V0 ⇒ V2 → ↑[O,1] V2 ≡ V →
    W0 ⇒ W2 → U0 ⇒ U2 →  𝕓{Abbr} W0. U0 ⇒ T1 →
    ∃∃X. 𝕗{Appl} V1. T1 ⇒ X & 𝕓{Abbr} W2. 𝕗{Appl} V. U2 ⇒ X.
-#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H 
+#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H
 elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2
 elim (lift_total VV 0 1) #VVV #HVV
 lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV
@@ -112,10 +112,30 @@ elim (tpr_inv_abbr1 … H) -H *
 [ -HV2 HVV2 #WW #UU #HWW0 #HUU0 #H destruct -T1;
   elim (IH … HW02 … HWW0) -HW02 HWW0 // #W #HW2 #HWW
   elim (IH … HU02 … HUU0) -HU02 HUU0 IH // #U #HU2 #HUU
+  @ex2_1_intro [2: @tpr_theta |1:skip |3: @tpr_bind ] /2 width=7/ (**) (* /4 width=7/ is too slow *)
+(* case 2: delta *)
+| -HV2 HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct -T1;
+  elim (IH … HW02 … HWW2) -HW02 HWW2 // #W #HW02 #HWW2
+  elim (IH … HU02 … HUU02) -HU02 HUU02 IH // #U #HU2 #HUUU2
+  elim (tpr_ps_bind … HWW2 HUUU2 … HUU2) -HUU2 HUUU2 #UUU #HUUU2 #HUUU1
   @ex2_1_intro
-  [2: @tpr_theta [5: @HVV1 |6: @HVV |7:// by {}; (*@HWW*) |8: @HUU |1,2,3,4:skip ]
-  |3: @tpr_bind [ @HW2 | @tpr_flat [ @HVVV | @HU2 ] ]
-  | skip 
+  [2: @tpr_theta
+  |1:skip
+  |3: @tpr_delta [3: @tpr_flat |1: skip ]
+  ] /2 width=14/ (**) (* /5 width=14/ is too slow *) 
+(* case 3: zeta *)
+| -HW02 HVV HVVV #UU1 #HUU10 #HUUT1
+  elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1
+  lapply (tw_lift … HUU10) -HUU10 #HUU10
+  elim (IH … HUUT1 … HUU1) -HUUT1 HUU1 IH // -HUU10 #U #HU2 #HUUU2
+  @ex2_1_intro
+  [2: @tpr_flat
+  |1: skip 
+  |3: @tpr_zeta [2: @lift_flat |1: skip |3: @tpr_flat ]
+  ] /2 width=5/ (**) (* /5 width=5/ is too slow *)
+]
+qed.
+
 (* Confluence ***************************************************************)
 
 lemma tpr_conf_aux:
@@ -155,120 +175,13 @@ lemma tpr_conf_aux:
   | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I
     @tpr_conf_flat_beta /2 width=8/ (**) (* /3 width=8/ is too slow *)
 (* case 8: flat, theta *)
-  | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I  
+  | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I
+    @tpr_conf_flat_theta /2 width=11/ (**) (* /3 width=11/ is too slow *)
+(* case 9: flat, tau *)
+  | #HT02 #H destruct -I
     //
+
 theorem tpr_conf: ∀T0,T1,T2. T0 ⇒ T1 → T0 ⇒ T2 →
                   ∃∃T. T1 ⇒ T & T2 ⇒ T.
 #T @(tw_wf_ind … T) -T /3 width=6/
 qed.
-*)
-lemma tpr_conf_aux:
-   ∀T. (
-      ∀T1. #T1 < #T → ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
-      ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
-         ) →
-   ∀U1,T1,U2,T2. U1 ⇒ T1 → U2 ⇒ T2 →
-   U1 = T → U2 = T →
-   ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
-#T #IH  #U1 #T1 #U2 #T2
-* -U1 T1
-[ #k1 * -U2 T2
-(* case 1: sort, sort *)
-  [ #k2 #H1 #H2 destruct -T k2 //
-(* case 2: sort, lref (excluded) *)
-  | #i2 #H1 #H2 destruct
-(* case 3: sort, bind (excluded) *)
-  | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
-(* case 4: sort, flat (excluded) *)
-  | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
-(* case 5: sort, beta (excluded) *)
-  | #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 destruct
-(* case 6: sort, delta (excluded) *)
-  | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct
-(* case 7: sort, theta (excluded) *)
-  | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 destruct
-(* case 8: sort, zeta (excluded) *)
-  | #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 destruct
-(* case 9: sort, tau (excluded) *)
-  | #V2 #T21 #T22 #_ #H1 #H2 destruct
-  ]
-| #i1 * -U2 T2
-(* case 10: lref, sort (excluded) broken *)
-  [ #k2 #H1 #H2 destruct
-(* case 11: lref, sort (excluded) *)
-  | #i2 #H1 #H2 destruct -T i2 //
-(* case 12: lref, bind (excluded) *)
-  | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
-(* case 13: lref, flat (excluded) *)
-  | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
-(* case 14: lref, beta (excluded) *)
-  | #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 destruct
-(* case 15: lref, delta (excluded) *)
-  | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct
-(* case 16: lref, theta (excluded) *)
-  | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 destruct
-(* case 17: lref, zeta (excluded) *)
-  | #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 destruct
-(* case 18: lref, tau (excluded) *)
-  | #V2 #T21 #T22 #_ #H1 #H2 destruct
-  ]
-| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -U2 T2
-(* case 19: bind, sort (excluded) *)
-  [ #k2 #H1 #H2 destruct
-(* case 20: bind, lref (excluded) *)
-  | #i2 #H1 #H2 destruct
-(* case 21: bind, bind *)
-  | #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2
-    destruct -T I2 V21 T21 /3 width=7/
-(* case 22: bind, flat (excluded) *)
-  | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
-(* case 23: bind, beta (excluded) *)
-  | #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 destruct
-(* case 24: bind, delta (excluded) *)
-  | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct
-(* case 25: bind, theta (excluded) *)
-  | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 destruct
-(* case 26: bind, zeta *)
-  | #V2 #T21 #T22 #T20 #HT212 #HT220 #H1 #H2
-    destruct -I1 V2 T21 T /3 width=8/
-(* case 27: bind, tau (excluded) *)
-  | #V2 #T21 #T22 #_ #H1 #H2 destruct
-  ]
-| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -U2 T2
-(* case 28: flat, sort (excluded) *)
-  [ #k2 #H1 #H2 destruct
-(* case 29: flat, lref (excluded) *)
-  | #i2 #H1 #H2 destruct
-(* case 30: flat, bind (excluded) *)
-  | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
-(* case 31: flat, flat *)
-  | #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2
-    destruct -T I2 V21 T21 /3 width=7/
-(* case 32: flat, beta *)
-  | #V21 #V22 #W2 #T21 #T22 #HV212 #HT212 #H1 #H2
-    destruct -I1 V21 T11 T /3 width=8/ (**) (* slow *)
-(* case 33: flat, delta (excluded) *)
-  | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct
-(* case 34: flat, theta *)
-  | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #H212 #HV222 #HW212 #HT212 #H1 #H2
-    destruct -I1 V21 T11 T //
-
-lemma tpr_conf_flat_theta:
-   ∀V11,V12,T12,V2,V22,W21,W22,T21,T22. (
-      ∀T1. #T1 < #V11 + (#W21 + #T21 + 1) + 1 →
-      ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
-      ∃∃T0. T3 ⇒ T0 & T4 ⇒T0
-   ) →
-   V11 ⇒ V12 → V11 ⇒ V22 → ↑[O,1] V22 ≡ V2 →
-   W21 ⇒ W22 → T21 ⇒ T22 →  𝕓{Abbr} W21. T21 ⇒ T12 →
-   ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} W22. 𝕗{Appl} V2. T22 ⇒T0.
-
-lemma tpr_conf_bind_delta:
-   ∀V0,V1,T0,T1,V2,T2,T. (
-      ∀X. #X < #V0 + #T0 + 1 →
-      ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
-      ∃∃X. X1 ⇒ X & X2⇒X
-   ) →
-   V0 ⇒ V1 → V0 ⇒ V2 →
-   T0 ⇒ T1 → T0 ⇒ T2 → ⋆. 𝕓{Abbr} V2 ⊢ T2 [O,1] ≫ T →
-   ∃∃X. 𝕓{Abbr} V1. T1 ⇒ X & 𝕓{Abbr} V2. T ⇒ X.
\ No newline at end of file
diff --git a/matita/matita/lib/lambda-delta/substitution/lift_defs.ma b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
index 472aef809..ff2545339 100644
--- a/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
@@ -27,7 +27,7 @@ inductive lift: term → nat → nat → term → Prop ≝
 
 interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2).
 
-(* The basic properties *****************************************************)
+(* Basic properties *********************************************************)
 
 lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d, e] #(i - e) ≡ #i.
 #d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3/
@@ -41,7 +41,7 @@ lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T.
 ]
 qed.
 
-(* The basic inversion lemmas ***********************************************)
+(* Basic inversion lemmas ***************************************************)
 
 lemma lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2.
 #d #e #T1 #T2 #H elim H -H d e T1 T2 /3/
@@ -51,10 +51,10 @@ lemma lift_inv_refl: ∀d,T1,T2. ↑[d, 0] T1 ≡ T2 → T1 = T2.
 /2/ qed.
 
 lemma lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k.
-#d #e #T1 #T2 #H elim H -H d e T1 T2 //
+#d #e #T1 #T2 * -d e T1 T2 //
 [ #i #d #e #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
 ]
 qed.
 
@@ -63,12 +63,12 @@ lemma lift_inv_sort1: ∀d,e,T2,k. ↑[d,e] ⋆k ≡ T2 → T2 = ⋆k.
 
 lemma lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i →
                           (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
-#d #e #T1 #T2 #H elim H -H d e T1 T2
+#d #e #T1 #T2 * -d e T1 T2
 [ #k #d #e #i #H destruct
 | #j #d #e #Hj #i #Hi destruct /3/
 | #j #d #e #Hj #i #Hi destruct /3/
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
 ]
 qed.
 
@@ -92,12 +92,12 @@ lemma lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
                           ∀I,V1,U1. T1 = 𝕓{I} V1.U1 →
                           ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
                                    T2 = 𝕓{I} V2. U2.
-#d #e #T1 #T2 #H elim H -H d e T1 T2
+#d #e #T1 #T2 * -d e T1 T2
 [ #k #d #e #I #V1 #U1 #H destruct
 | #i #d #e #_ #I #V1 #U1 #H destruct
 | #i #d #e #_ #I #V1 #U1 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V1 #U1 #H destruct /2 width=5/
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V1 #U1 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct
 ]
 qed.
 
@@ -110,12 +110,12 @@ lemma lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
                           ∀I,V1,U1. T1 = 𝕗{I} V1.U1 →
                           ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
                                    T2 = 𝕗{I} V2. U2.
-#d #e #T1 #T2 #H elim H -H d e T1 T2
+#d #e #T1 #T2 * -d e T1 T2
 [ #k #d #e #I #V1 #U1 #H destruct
 | #i #d #e #_ #I #V1 #U1 #H destruct
 | #i #d #e #_ #I #V1 #U1 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V1 #U1 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V1 #U1 #H destruct /2 width=5/
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/
 ]
 qed.
 
@@ -125,10 +125,10 @@ lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕗{I} V1. U1 ≡ T2 →
 /2/ qed.
 
 lemma lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
-#d #e #T1 #T2 #H elim H -H d e T1 T2 //
+#d #e #T1 #T2 * -d e T1 T2 //
 [ #i #d #e #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
 ]
 qed.
 
@@ -137,12 +137,12 @@ lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k.
 
 lemma lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i →
                           (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
-#d #e #T1 #T2 #H elim H -H d e T1 T2
+#d #e #T1 #T2 * -d e T1 T2
 [ #k #d #e #i #H destruct
 | #j #d #e #Hj #i #Hi destruct /3/
 | #j #d #e #Hj #i #Hi destruct <minus_plus_m_m /4/
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
 ]
 qed.
 
@@ -166,12 +166,12 @@ lemma lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
                           ∀I,V2,U2. T2 = 𝕓{I} V2.U2 →
                           ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
                                    T1 = 𝕓{I} V1. U1.
-#d #e #T1 #T2 #H elim H -H d e T1 T2
+#d #e #T1 #T2 * -d e T1 T2
 [ #k #d #e #I #V2 #U2 #H destruct
 | #i #d #e #_ #I #V2 #U2 #H destruct
 | #i #d #e #_ #I #V2 #U2 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct /2 width=5/
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct /2 width=5/
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct
 ]
 qed.
 
@@ -184,12 +184,12 @@ lemma lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
                           ∀I,V2,U2. T2 = 𝕗{I} V2.U2 →
                           ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
                                    T1 = 𝕗{I} V1. U1.
-#d #e #T1 #T2 #H elim H -H d e T1 T2
+#d #e #T1 #T2 * -d e T1 T2
 [ #k #d #e #I #V2 #U2 #H destruct
 | #i #d #e #_ #I #V2 #U2 #H destruct
 | #i #d #e #_ #I #V2 #U2 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct /2 width = 5/
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct /2 width = 5/
 ]
 qed.
 
diff --git a/matita/matita/lib/lambda-delta/substitution/lift_fun.ma b/matita/matita/lib/lambda-delta/substitution/lift_fun.ma
index 0044de7f1..58d718fb7 100644
--- a/matita/matita/lib/lambda-delta/substitution/lift_fun.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift_fun.ma
@@ -16,7 +16,7 @@ include "lambda-delta/substitution/lift_defs.ma".
 
 (* RELOCATION ***************************************************************)
 
-(* the functional properties ************************************************)
+(* Functional properties ****************************************************)
 
 lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2.
 #T1 elim T1 -T1
diff --git a/matita/matita/lib/lambda-delta/substitution/lift_main.ma b/matita/matita/lib/lambda-delta/substitution/lift_main.ma
index a41e49c5b..5ef9a31f4 100644
--- a/matita/matita/lib/lambda-delta/substitution/lift_main.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift_main.ma
@@ -16,7 +16,7 @@ include "lambda-delta/substitution/lift_defs.ma".
 
 (* RELOCATION ***************************************************************)
 
-(* the main properies *******************************************************)
+(* Main properies ***********************************************************)
 
 lemma lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
                    ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T →
diff --git a/matita/matita/lib/lambda-delta/syntax/item.ma b/matita/matita/lib/lambda-delta/syntax/item.ma
index ea7a45362..c9673b47e 100644
--- a/matita/matita/lib/lambda-delta/syntax/item.ma
+++ b/matita/matita/lib/lambda-delta/syntax/item.ma
@@ -16,6 +16,8 @@
  *)
 
 include "lambda-delta/ground.ma".
+include "lambda-delta/xoa_defs.ma".
+include "lambda-delta/xoa_notation.ma".
 include "lambda-delta/notation.ma".
 
 (* BINARY ITEMS *************************************************************)
diff --git a/matita/matita/lib/lambda-delta/xoa_defs.ma b/matita/matita/lib/lambda-delta/xoa_defs.ma
index 9dbf226f4..68a0776dc 100644
--- a/matita/matita/lib/lambda-delta/xoa_defs.ma
+++ b/matita/matita/lib/lambda-delta/xoa_defs.ma
@@ -16,72 +16,96 @@
 
 include "basics/pts.ma".
 
+(* multiple existental quantifier (2, 1) *)
+
 inductive ex2_1 (A0:Type[0]) (P0,P1:A0→Prop) : Prop ≝
    | ex2_1_intro: ∀x0. P0 x0 → P1 x0 → ex2_1 ? ? ?
 .
 
 interpretation "multiple existental quantifier (2, 1)" 'Ex P0 P1 = (ex2_1 ? P0 P1).
 
+(* multiple existental quantifier (2, 2) *)
+
 inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝
    | ex2_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → ex2_2 ? ? ? ?
 .
 
 interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1).
 
+(* multiple existental quantifier (3, 1) *)
+
 inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝
    | ex3_1_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3_1 ? ? ? ?
 .
 
 interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3_1 ? P0 P1 P2).
 
+(* multiple existental quantifier (3, 2) *)
+
 inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝
    | ex3_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → ex3_2 ? ? ? ? ?
 .
 
 interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2).
 
+(* multiple existental quantifier (3, 3) *)
+
 inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝
    | ex3_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → ex3_3 ? ? ? ? ? ?
 .
 
 interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2).
 
+(* multiple existental quantifier (4, 3) *)
+
 inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝
    | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ?
 .
 
 interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3).
 
+(* multiple existental quantifier (4, 4) *)
+
 inductive ex4_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→Prop) : Prop ≝
    | ex4_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → ex4_4 ? ? ? ? ? ? ? ?
 .
 
 interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3).
 
+(* multiple existental quantifier (5, 3) *)
+
 inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→Prop) : Prop ≝
    | ex5_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → ex5_3 ? ? ? ? ? ? ? ?
 .
 
 interpretation "multiple existental quantifier (5, 3)" 'Ex P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4).
 
+(* multiple existental quantifier (5, 4) *)
+
 inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→Prop) : Prop ≝
    | ex5_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → ex5_4 ? ? ? ? ? ? ? ? ?
 .
 
 interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4).
 
+(* multiple existental quantifier (6, 6) *)
+
 inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝
    | ex6_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → ex6_6 ? ? ? ? ? ? ? ? ? ? ? ?
 .
 
 interpretation "multiple existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5).
 
+(* multiple existental quantifier (7, 6) *)
+
 inductive ex7_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝
    | ex7_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → P6 x0 x1 x2 x3 x4 x5 → ex7_6 ? ? ? ? ? ? ? ? ? ? ? ? ?
 .
 
 interpretation "multiple existental quantifier (7, 6)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
 
+(* multiple disjunction connective (3) *)
+
 inductive or3 (P0,P1,P2:Prop) : Prop ≝
    | or3_intro0: P0 → or3 ? ? ?
    | or3_intro1: P1 → or3 ? ? ?
@@ -90,6 +114,8 @@ inductive or3 (P0,P1,P2:Prop) : Prop ≝
 
 interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2).
 
+(* multiple disjunction connective (4) *)
+
 inductive or4 (P0,P1,P2,P3:Prop) : Prop ≝
    | or4_intro0: P0 → or4 ? ? ? ?
    | or4_intro1: P1 → or4 ? ? ? ?
diff --git a/matita/matita/lib/lambda-delta/xoa_notation.ma b/matita/matita/lib/lambda-delta/xoa_notation.ma
index e37c37eb1..b8270b660 100644
--- a/matita/matita/lib/lambda-delta/xoa_notation.ma
+++ b/matita/matita/lib/lambda-delta/xoa_notation.ma
@@ -14,54 +14,124 @@
 
 (* This file was generated by xoa.native: do not edit *********************)
 
-notation "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
+(* multiple existental quantifier (2, 1) *)
+
+notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) }.
 
-notation "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)"
+notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
  non associative with precedence 20
- for @{ 'Ex (λ${ident x0},${ident x1}.$P0) (λ${ident x0},${ident x1}.$P1) }.
+ for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) }.
+
+(* multiple existental quantifier (2, 2) *)
 
-notation "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }.
+
+(* multiple existental quantifier (3, 1) *)
+
+notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) }.
 
-notation "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) }.
+
+(* multiple existental quantifier (3, 2) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
  non associative with precedence 20
- for @{ 'Ex (λ${ident x0},${ident x1}.$P0) (λ${ident x0},${ident x1}.$P1) (λ${ident x0},${ident x1}.$P2) }.
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) }.
 
-notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
  non associative with precedence 20
- for @{ 'Ex (λ${ident x0},${ident x1},${ident x2}.$P0) (λ${ident x0},${ident x1},${ident x2}.$P1) (λ${ident x0},${ident x1},${ident x2}.$P2) }.
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }.
+
+(* multiple existental quantifier (3, 3) *)
 
-notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
  non associative with precedence 20
- for @{ 'Ex (λ${ident x0},${ident x1},${ident x2}.$P0) (λ${ident x0},${ident x1},${ident x2}.$P1) (λ${ident x0},${ident x1},${ident x2}.$P2) (λ${ident x0},${ident x1},${ident x2}.$P3) }.
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) }.
 
-notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
  non associative with precedence 20
- for @{ 'Ex (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P0) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P1) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P2) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P3) }.
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }.
+
+(* multiple existental quantifier (4, 3) *)
 
-notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
  non associative with precedence 20
- for @{ 'Ex (λ${ident x0},${ident x1},${ident x2}.$P0) (λ${ident x0},${ident x1},${ident x2}.$P1) (λ${ident x0},${ident x1},${ident x2}.$P2) (λ${ident x0},${ident x1},${ident x2}.$P3) (λ${ident x0},${ident x1},${ident x2}.$P4) }.
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) }.
 
-notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
  non associative with precedence 20
- for @{ 'Ex (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P0) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P1) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P2) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P3) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P4) }.
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) }.
+
+(* multiple existental quantifier (4, 4) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) }.
+
+(* multiple existental quantifier (5, 3) *)
 
-notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
  non associative with precedence 20
- for @{ 'Ex (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P0) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P1) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P2) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P3) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P4) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P5) }.
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) }.
 
-notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
  non associative with precedence 20
- for @{ 'Ex (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P0) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P1) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P2) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P3) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P4) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P5) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P6) }.
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) }.
+
+(* multiple existental quantifier (5, 4) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) }.
+
+(* multiple existental quantifier (6, 6) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P5) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P5) }.
+
+(* multiple existental quantifier (7, 6) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P6) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P6) }.
+
+(* multiple disjunction connective (3) *)
 
 notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2)"
  non associative with precedence 30
  for @{ 'Or $P0 $P1 $P2 }.
 
+(* multiple disjunction connective (4) *)
+
 notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break | term 29 P3)"
  non associative with precedence 30
  for @{ 'Or $P0 $P1 $P2 $P3 }.