From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 13 Nov 2012 20:50:33 +0000 (+0000)
Subject: - one axiom removed from sd
X-Git-Tag: make_still_working~1470
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6c86c70b005e3f3efd375868b27f3cff84febfad;p=helm.git

- one axiom removed from sd
- traces added to auto to make it work
- bugfix in Makefile
- more notation and existentials for staff to be committed
- some minor additions
---

diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile
index 7d2fee6bf..3e696b6b6 100644
--- a/matita/matita/contribs/lambda_delta/Makefile
+++ b/matita/matita/contribs/lambda_delta/Makefile
@@ -19,7 +19,7 @@ all:
 
 # xoa ########################################################################
 
-xoa: $(TARGETS)
+xoa: $(XOA_TARGETS)
 
 $(XOA_TARGETS): $(XOA_CONF)
 	@echo "  EXEC $(XOA) $(XOA_CONF)"
@@ -106,7 +106,7 @@ define SUMMARY_TEMPLATE
 	@printf '   ]\n'                               >> $$@
 	@printf '   class "cyan" [ "sizes"\n'          >> $$@
 	@printf '      [ "files" "$$(V1)" ]\n'         >> $$@
-	@printf '      [ "bytes" "$$(V2)" ]\n'         >> $$@
+	@printf '      [ "characters" "$$(V2)" ]\n'    >> $$@
 	@printf '      [ * ]\n'                        >> $$@
 	@printf '   ]\n'                               >> $$@	
 	@printf '   class "green" [ "propositions"\n'  >> $$@
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma
index 34e93db9d..854c5da27 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/static/lsubss.ma".
 include "basic_2/reducibility/xpr.ma".
 (*
 include "basic_2/reducibility/cnf.ma".
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lsubss.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lsubss.ma
new file mode 100644
index 000000000..c883c14f3
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lsubss.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/reducibility/xpr_lsubss.ma".
+include "basic_2/computation/xprs.ma".
+
+(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************)
+
+(* Properties on lenv ref for stratified type assignment ********************)
+
+lemma lsubss_xprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+                         ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •➡*[g] T2.
+#h #g #L1 #L2 #HL12 #T1 #T2 #H @(xprs_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT1
+lapply (lsubss_xpr_trans … HL12 … HT2) -L2 /2 width=3/
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma
index a934ca08e..bd6b2121d 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/static/ssta.ma".
 include "basic_2/dynamic/snv.ma".
 
 (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
@@ -31,23 +30,16 @@ lemma snv_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃∃U,l. ⦃h, L⦄ ⊢
 | #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *) 
 ]
 qed-.
-(*
+
 fact snv_ssta_conf_aux: ∀h,g,L,T. (
-                           ∀L0,T1,U1,l1. ⦃h, L0⦄ ⊢ T1 •[g, l1] U1 →
-                           ∀T2,U2,l2. ⦃h, L0⦄ ⊢ T2 •[g, l2] U2 →
-                           L0 ⊢ T1 ⬌* T2 → ⦃h, L0⦄ ⊩ T1 :[g] →  ⦃h, L0⦄ ⊩ T2 :[g] →
-                           #{L0, T1} < #{L ,T} →
-                           l1 = l2 ∧ L0 ⊢ U1 ⬌* U2
-                        ) → (
                            ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] →
                            ∀U0. ⦃h, L0⦄ ⊢ T0 •➡*[g] U0 →
-                           #{L0, T0} < #{L ,T} →
-                           ⦃h, L0⦄ ⊩ U0 :[g]
+                           #{L0, T0} < #{L ,T} → ⦃h, L0⦄ ⊩ U0 :[g]
                         ) →
                         ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] →
-                        ∀U0,l. ⦃h, L⦄ ⊢ T0 •[g, l + 1] U0 →
+                        ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 →
                         L0 = L → T0 = T → ⦃h, L0⦄ ⊩ U0 :[g].
-#h #g #L #T #IH2 #IH1 #L0 #T0 * -L0 -T0
+#h #g #L #T #IH1 #L0 #T0 * -L0 -T0
 [
 |
 |
@@ -55,13 +47,6 @@ fact snv_ssta_conf_aux: ∀h,g,L,T. (
   elim (ssta_inv_appl1 … H) -H #U0 #HTU0 #H destruct
   lapply (IH1 … HT0 U0 ? ?) // [ /3 width=2/ ] -HTU0 #HU0
   @(snv_appl … HV HU0 HVW HW0) -HV -HU0 -HVW -HW0
-| #L0 #W #T0 #W0 #l0 #HW #HT0 #HTW0 #HW0 #X #l #H #H1 #H2 destruct
-  elim (ssta_inv_cast1 … H) -H <minus_plus_m_m #V #U0 #HWV #HTU0 #H destruct
-  elim (ssta_mono … HTU0 … HTW0) -HTU0 #H1 #H2
-  lapply (injective_plus_l … H1) -H1 #H1 destruct
-(*  elim (ssta_fwd_correct … HTW0) <minus_plus_m_m #X0 #HWX0 *)
-  lapply (IH1 … HT0 W0 ? ?) -IH1 -HT0 // [ /3 width=2/ ] -HTW0 #HW0
-  @(snv_cast … HV HW0) 
-  
-  HVW HW0) -HV -HU0 -HVW -HW0  
-*)
+| #L0 #W #T0 #W0 #l0 #_ #HT0 #_ #_ #U0 #l #H #H1 #H2 destruct -W0
+  lapply (ssta_inv_cast1 … H) -H #HTU0
+  lapply (IH1 … HT0 U0 ? ?) -IH1 -HT0 // -W /3 width=2/
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma
index 478911825..d9569d4d5 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma
@@ -42,20 +42,25 @@ lemma tw_shift: ∀L,T. #{L, T} ≤ #{L @@ T}.
 qed.
 
 lemma fw_tpair_sn: ∀I,L,V,T. #{L, V} < #{L, ②{I}V.T}.
-#I #L #V #T normalize in ⊢ (? % %); //
+normalize in ⊢ (?→?→?→?→?%%); //
 qed.
 
 lemma fw_tpair_dx: ∀I,L,V,T. #{L, T} < #{L, ②{I}V.T}.
-#I #L #V #T normalize in ⊢ (? % %); //
+normalize in ⊢ (?→?→?→?→?%%); //
 qed.
 
 lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #{L, V2} < #{L, ②{I1}V1.②{I2}V2.T}.
-#I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/
+normalize in ⊢ (?→?→?→?→?→?→?%%); /2 width=1/
 qed.
 
-lemma fw_tpair_dx_sn_shift: ∀a2,I1,I2,L,V1,V2,T.
-                            #{L.ⓑ{I2}V2, T} < #{L, ②{I1}V1.ⓑ{a2,I2}V2.T}.
-#a2 #I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/
+lemma fw_tpair_sn_sn_shift: ∀I,I1,I2,L,V1,V2,T.
+                            #{L.ⓑ{I}V1, T} < #{L, ②{I1}V1.②{I2}V2.T}.
+normalize in ⊢ (?→?→?→?→?→?→?→?%%); /3 width=1/ 
+qed.
+
+lemma fw_tpair_sn_dx_shift: ∀I,I1,I2,L,V1,V2,T.
+                            #{L.ⓑ{I}V2, T} < #{L, ②{I1}V1.②{I2}V2.T}.
+normalize in ⊢ (?→?→?→?→?→?→?→?%%); /2 width=1/
 qed.
 
 (* Basic_1: removed theorems 6:
diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index affb8af13..bba14af32 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -258,10 +258,6 @@ notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • break [ g , break
    non associative with precedence 45
    for @{ 'StaticType $h $g $l $L $T1 $T2 }.
 
-notation "hvbox( h ⊢ break term 46 L1 • ≃ [ g ] break term 46 L2 )"
-   non associative with precedence 45
-   for @{ 'CCongS $h $g $L1 $L2 }.
-
 notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ g ] break term 46 L2 )"
    non associative with precedence 45
    for @{ 'CrSubEqS $h $g $L1 $L2 }.
@@ -456,6 +452,10 @@ notation "hvbox( ⦃ h , break L ⦄ ⊩ break term 46 T : break [ g ] )"
    non associative with precedence 45
    for @{ 'NativeValid $h $g $L $T }.
 
+notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ [ g ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'CrSubEqV $h $g $L1 $L2 }.
+
 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break term 46 T2 )"
    non associative with precedence 45
    for @{ 'NativeType $h $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lsubss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lsubss.ma
new file mode 100644
index 000000000..bc66cd2cd
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lsubss.ma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/lsubss_ssta.ma".
+include "basic_2/reducibility/xpr.ma".
+
+(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************)
+
+(* Properties on lenv ref for stratified type assignment ********************)
+
+lemma lsubss_xpr_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+                        ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •➡[g] T2 → ⦃h, L1⦄ ⊢ T1 •➡[g] T2.
+#h #g #L1 #L2 #HL12 #T1 #T2 * [ | #l ] #HT12
+[ lapply (lsubss_fwd_lsubs2 … HL12) -HL12 /3 width=3/
+| /3 width=4/
+]
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sd.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sd.ma
index 04adbae95..63143b19b 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/static/sd.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/sd.ma
@@ -18,11 +18,10 @@ include "basic_2/static/sh.ma".
 
 (* sort degree specification *)
 record sd (h:sh): Type[0] ≝ {
-   deg      : relation nat;                                 (* degree of the sort *)
-   deg_total: ∀k. ∃l. deg k l;                              (* functional relation axioms *)
+   deg      : relation nat;                            (* degree of the sort *)
+   deg_total: ∀k. ∃l. deg k l;                         (* functional relation axioms *)
    deg_mono : ∀k,l1,l2. deg k l1 → deg k l2 → l1 = l2;
-   deg_next : ∀k,l. deg k l → deg (next h k) (l - 1);       (* compatibility condition *)
-   deg_prev : ∀k,l. deg (next h k) (l + 1) → deg k (l + 2)
+   deg_next : ∀k,l. deg k l → deg (next h k) (l - 1)   (* compatibility condition *)
 }.
 
 (* Notable specifications ***************************************************)
@@ -79,9 +78,6 @@ definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) ….
   | #H1 @deg_SO_zero * #l #H2 destruct
     @H1 -H1 @(ex_intro … (S l)) /2 width=1/ (**) (* explicit constructor *)
   ]
-| #K0 #l0 #H
-  <(deg_SO_inv_pos … H) -H >plus_n_2
-  @deg_SO_pos >iter_SO /2 width=1/ (**) (* explicit constructor: iter_SO is needed *)
 ]
 qed.
 
@@ -96,6 +92,14 @@ let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝
 
 (* Basic properties *********************************************************)
 
+lemma deg_pred: ∀h,g,k,l. deg h g (next h k) (l + 1) → deg h g k (l + 2).
+#h #g #k #l #H1
+elim (deg_total h g k) #l0 #H0
+lapply (deg_next … H0) #H2
+lapply (deg_mono … H1 H2) -H1 -H2 #H
+<(associative_plus l 1 1) >H <plus_minus_m_m // /2 width=3 by transitive_le/
+qed.
+
 lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1).
 #h #k #l <plus_n_Sm <plus_n_Sm //
 qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups.ma
index 9d216beca..5923d60a3 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/frsups.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/frsup.ma".
 include "basic_2/unfold/frsupp.ma".
 
 (* STAR-ITERATED RESTRICTED SUPCLOSURE **************************************)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma
index d9d704221..6ba09b962 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma
@@ -202,7 +202,8 @@ lemma ltpss_dx_weak: ∀L1,L2,d1,e1. L1 ▶* [d1, e1] L2 →
     lapply (le_plus_to_minus … Hd21) -Hd21 #Hd21 /3 width=5/
   | -Hd21 normalize in Hde12;
     lapply (lt_to_le_to_lt 0 … Hde12) // #He2
-    lapply (le_plus_to_minus_r … Hde12) -Hde12 /3 width=5/
+    lapply (le_plus_to_minus_r … Hde12) -Hde12
+    /3 width=5 by ltpss_dx_tpss2_lt, tpss_weak/ (**) (* /3 width=5/ used to work *)
   ]
 ]
 qed.
diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml
index c150f4503..edf66e433 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml
+++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml
@@ -35,6 +35,7 @@
     <key name="ex">6 4</key>
     <key name="ex">6 6</key>
     <key name="ex">6 7</key>
+    <key name="ex">7 4</key>
     <key name="ex">7 7</key>
     <key name="or">3</key>
     <key name="or">4</key>
diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
index f4296024f..9da161d42 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
@@ -184,6 +184,14 @@ inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2
 
 interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5).
 
+(* multiple existental quantifier (7, 4) *)
+
+inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝
+   | ex7_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 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+
 (* multiple existental quantifier (7, 7) *)
 
 inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝
diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma
index ed4b83f83..9e2f4d099 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma
@@ -224,6 +224,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 ,
  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.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }.
 
+(* multiple existental quantifier (7, 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 break & term 19 P5 break & term 19 P6)"
+ 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) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) }.
+
+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 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.$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) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }.
+
 (* multiple existental quantifier (7, 7) *)
 
 notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 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)"