- inversion lemmas for tpr completed!

- bug fix in lpr interpretation

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index d39b3faf46667050c302cd13a535595b9e383a21..54f9da02a162a1e307e99a4e72ea143c9dbfbe22 100644 (file)
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -21,6 +21,12 @@ lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
 lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
 // qed.
 
+lemma arith8: ∀a,b. a < a + b + 1.
+// qed.
+
+lemma arith9: ∀a,b,c. c < a + (b + c + 1) + 1.
+// qed.
+
 lemma minus_le: ∀m,n. m - n ≤ m.
 /2/ qed.
 

diff --git a/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma
index dab96f2dd871a19a0c8d47a543d8dc8f6ef2f2e9..2411191084e4856e99c3704b8ecf3bcc2f6b5fa6 100644 (file)
--- a/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma
+++ b/matita/matita/lib/lambda-delta/reduction/lpr_defs.ma
@@ -24,7 +24,7 @@ inductive lpr: lenv → lenv → Prop ≝
 
 interpretation
   "context-free parallel reduction (environment)"
-  'PR L1 L2 = (lpr L1 L2).
+  'PRed L1 L2 = (lpr L1 L2).
 
 (* Basic inversion lemmas ***************************************************)
 

diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
index bddd93017bf8851b2e731b81c3d0c9ce964db7b5..498fbb744c5b567a5e2acecd15f993daa4f9c205 100644 (file)
--- a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
+++ b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
@@ -45,23 +45,160 @@ lemma tpr_refl: ∀T. T ⇒ T.
 #I elim I -I /2/
 qed.
 
-(* The basic inversion lemmas ***********************************************)
+(* Basic inversion lemmas ***************************************************)
+
+lemma tpr_inv_sort1_aux: ∀U1,U2. U1 ⇒ U2 → ∀k. U1 = ⋆k → U2 = ⋆k.
+#U1 #U2 * -U1 U2
+[ #k0 #k #H destruct -k0 //
+| #i #k #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
+| #V #T #T1 #T2 #_ #_ #k #H destruct
+| #V #T1 #T2 #_ #k #H destruct
+]
+qed.
+
+lemma tpr_inv_sort1: ∀k,U2. ⋆k ⇒ U2 → U2 = ⋆k.
+/2/ qed.
+
+lemma tpr_inv_lref1_aux: ∀U1,U2. U1 ⇒ U2 → ∀i. U1 = #i → U2 = #i.
+#U1 #U2 * -U1 U2
+[ #k #i #H destruct
+| #j #i #H destruct -j //
+| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
+| #V #T #T1 #T2 #_ #_ #i #H destruct
+| #V #T1 #T2 #_ #i #H destruct
+]
+qed.
+
+lemma tpr_inv_lref1: ∀i,U2. #i ⇒ U2 → U2 = #i.
+/2/ qed.
+
+lemma tpr_inv_abbr1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abbr} V1. T1 →
+                         ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abbr} V2. T2
+                          | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
+                                       ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
+                                       U2 = 𝕚{Abbr} V2. T
+                          | ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
+#U1 #U2 * -U1 U2
+[ #k #V #T #H destruct
+| #i #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
+| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
+| #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -V1 T1 /3 width=7/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
+| #V #T #T1 #T2 #HT1 #HT12 #V0 #T0 #H destruct -V T /3/
+| #V #T1 #T2 #_ #V0 #T0 #H destruct
+]
+qed.
+
+lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕚{Abbr} V1. T1 ⇒ U2 →
+                     ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abbr} V2. T2
+                      | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
+                                   ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
+                                   U2 = 𝕚{Abbr} V2. T
+                      | ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2.
+/2/ qed.
+
+lemma tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 →
+                         ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
+#U1 #U2 * -U1 U2
+[ #k #V #T #H destruct
+| #i #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /2 width=5/
+| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
+| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
+| #V #T1 #T2 #_ #V0 #T0 #H destruct
+]
+qed.
+
+lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕚{Abst} V1. T1 ⇒ U2 →
+                     ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
+/2/ qed.
+
+lemma tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U0 →
+                         ∨∨ ∃∃V2,T2.            V1 ⇒ V2 & U0 ⇒ T2 &
+                                                U2 = 𝕚{Appl} V2. T2
+                          | ∃∃V2,W,T1,T2.       V1 ⇒ V2 & T1 ⇒ T2 &
+                                                U0 = 𝕚{Abst} W. T1 &
+                                                U2 = 𝕓{Abbr} V2. T2
+                          | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
+                                                ↑[0,1] V2 ≡ V &
+                                                U0 = 𝕚{Abbr} W1. T1 &
+                                                U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2.
+#U1 #U2 * -U1 U2
+[ #k #V #T #H destruct
+| #i #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
+| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #V #T #H destruct -V1 T /3 width=8/
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #V0 #T0 #H
+  destruct -V1 T0 /3 width=12/
+| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
+| #V #T1 #T2 #_ #V0 #T0 #H destruct
+]
+qed.
+
+lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕚{Appl} V1. U0 ⇒ U2 →
+                     ∨∨ ∃∃V2,T2.            V1 ⇒ V2 & U0 ⇒ T2 &
+                                            U2 = 𝕚{Appl} V2. T2
+                      | ∃∃V2,W,T1,T2.       V1 ⇒ V2 & T1 ⇒ T2 &
+                                            U0 = 𝕚{Abst} W. T1 &
+                                            U2 = 𝕓{Abbr} V2. T2
+                      | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
+                                            ↑[0,1] V2 ≡ V &
+                                            U0 = 𝕚{Abbr} W1. T1 &
+                                            U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2.
+/2/ qed.
+
+lemma tpr_inv_cast1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Cast} V1. T1 →
+                           (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2)
+                         ∨ T1 ⇒ U2.
+#U1 #U2 * -U1 U2
+[ #k #V #T #H destruct
+| #i #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
+| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
+| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
+| #V #T1 #T2 #HT12 #V0 #T0 #H destruct -V T1 /2/
+]
+qed.
+
+lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕚{Cast} V1. T1 ⇒ U2 →
+                       (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2)
+                     ∨ T1 ⇒ U2.
+/2/ qed.
 
 lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
                          ∨∨           T1 = #i
                           | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
-                                      T1 = ð\9d\95\93{Abbr} V. T
-                          | â\88\83â\88\83V,T.    T â\87\92 #i & T1 = ð\9d\95\97{Cast} V. T.
-#T1 #T2 #H elim H -H T1 T2
+                                      T1 = ð\9d\95\9a{Abbr} V. T
+                          | â\88\83â\88\83V,T.    T â\87\92 #i & T1 = ð\9d\95\9a{Cast} V. T.
+#T1 #T2 * -T1 T2
 [ #k #i #H destruct
 | #j #i /2/
-| #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #_ #_ #i #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #i #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #_ #i #H destruct /3 width=6/
-| #V #T1 #T2 #HT12 #_ #i #H destruct /3/
+| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
+| #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
+| #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
+| #V #T1 #T2 #HT12 #i #H destruct /3/
 ]
 qed.
 

diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
index 4451ec892373030d917b7a11d4098653885409a8..2bc32505ff32b58de7a8196c92b0747c5e729458 100644 (file)
--- a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
+++ b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
@@ -33,8 +33,7 @@ lemma tpr_conf_bind_bind:
    ∃∃T0. 𝕓{I1} V12. T12 ⇒ T0 & 𝕓{I1} V22. T22 ⇒ T0.
 #I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
 elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2
-elim (IH … HT1 … HT2) -HT1 HT2 // #T #HT1 #HT2
-/3 width=5/
+elim (IH … HT1 … HT2) -HT1 HT2 IH /3 width=5/
 qed.
 
 lemma tpr_conf_bind_zeta:
@@ -62,10 +61,35 @@ lemma tpr_conf_flat_flat:
    ∃∃T0. 𝕗{I1} V12. T12 ⇒ T0 & 𝕗{I1} V22. T22 ⇒ T0.
 #I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
 elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2
-elim (IH … HT1 … HT2) -HT1 HT2 // #T #HT1 #HT2
-/3 width=5/
+elim (IH … HT1 … HT2) -HT1 HT2 /3 width=5/
 qed.
 
+lemma tpr_conf_flat_beta:
+   ∀V11,V12,T12,V22,W2,T21,T22. (
+      ∀T1. #T1 < #V11 + (#W2 + #T21 + 1) + 1 →
+      ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
+      ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+   ) →
+   V11 ⇒ V12 → V11 ⇒ V22 →
+   T21 ⇒ T22 → 𝕓{Abst} W2. T21 ⇒ T12 →
+   ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} V22. T22 ⇒ T0.
+#V11 #V12 #T12 #V22 #W2 #T21 #T22 #IH #HV1 #HV2 #HT1 #HT2
+elim (tpr_inv_abst1 … HT2) -HT2 #W1 #T1 #HW21 #HT21 #H destruct -T12;
+elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV12 #HV22
+elim (IH … HT21 … HT1) -HT21 HT1 IH /3 width=5/
+qed.
+
+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.
+
+
 (* Confluence ***************************************************************)
 
 lemma tpr_conf_aux:
@@ -140,7 +164,7 @@ lemma tpr_conf_aux:
 (* case 27: bind, tau (excluded) *)
   | #V2 #T21 #T22 #_ #H1 #H2 destruct
   ]
-| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -U2 T2 
+| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -U2 T2
 (* case 28: flat, sort (excluded) *)
   [ #k2 #H1 #H2 destruct
 (* case 29: flat, lref (excluded) *)
@@ -152,9 +176,24 @@ lemma tpr_conf_aux:
     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; 
-  
-theorem pr_conf: ∀T,T1,T2. T ⇒ T1 → T ⇒ T2 →
+    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.
+
+theorem tpr_conf: ∀T,T1,T2. T ⇒ T1 → T ⇒ T2 →
                  ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
 #T @(tw_wf_ind … T) -T /3 width=8/
 qed.

diff --git a/matita/matita/lib/lambda-delta/xoa_defs.ma b/matita/matita/lib/lambda-delta/xoa_defs.ma
index 5e66ef7899ffbeb04aaa38d85dd7b1183185d078..af9ba3708627092d7d1ee6387e5c91c18bbea241 100644 (file)
--- a/matita/matita/lib/lambda-delta/xoa_defs.ma
+++ b/matita/matita/lib/lambda-delta/xoa_defs.ma
@@ -40,6 +40,24 @@ inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝
 
 interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2).
 
+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).
+
+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).
+
+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).
+
 inductive or3 (P0,P1,P2:Prop) : Prop ≝
    | or3_intro0: P0 → or3 ? ? ?
    | or3_intro1: P1 → or3 ? ? ?

diff --git a/matita/matita/lib/lambda-delta/xoa_notation.ma b/matita/matita/lib/lambda-delta/xoa_notation.ma
index f21488be3f086d0b8b4e219e43bd27bbb7b2a2d3..18b3c0293ea3db8b5715b7aef268568a469cc665 100644 (file)
--- a/matita/matita/lib/lambda-delta/xoa_notation.ma
+++ b/matita/matita/lib/lambda-delta/xoa_notation.ma
@@ -30,6 +30,18 @@ notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break &
  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) }.
 
+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) }.
+
+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 , 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(∨∨ term 19 P0 break | term 19 P1 break | term 19 P2)"
  non associative with precedence 20
  for @{ 'Or $P0 $P1 $P2 }.