#m #n elim (decidable_lt m n) /3/
qed.
-lemma lt_false: ∀n. n < n → False.
-#n #H lapply (lt_to_not_eq … H) -H #H elim H -H /2/
+lemma lt_refl_false: ∀n. n < n → False.
+#n #H elim (lt_to_not_eq … H) -H /2/
+qed.
+
+lemma lt_zero_false: ∀n. n < 0 → False.
+#n #H elim (lt_to_not_le … H) -H /2/
qed.
lemma plus_lt_false: ∀m,n. m + n < m → False.
#m #n #H1 lapply (le_plus_n_r n m) #H2
lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
-elim (lt_false … H)
+elim (lt_refl_false … H)
qed.
lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
lemma arith5: ∀i,h,d. i + h ≤ d → d - i - h + (i + h) = d.
/2/ qed.
+
+lemma arith6: ∀m,n. m < n → n - (n - m - 1) = m + 1.
+#m #n #H >minus_plus <minus_minus //
+qed.
+
+lemma arith7: ∀i,d. i ≤ d → d - i + i = d.
+/2/ qed.
#T elim T -T //
#I elim I -I /2/
qed.
+
+(* The basic inversion lemmas ***********************************************)
+
+lemma pr_inv_lref2_aux: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → ∀i. T2 = #i →
+ ∨∨ T1 = #i
+ | ∃∃K,V1,j. j < i & K ⊢ V1 ⇒ #(i-j-1) &
+ ↑[O,j] K. 𝕓{Abbr} V1 ≡ L & T1 = #j
+ | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & L ⊢ T0 ⇒ #i &
+ T1 = 𝕓{Abbr} V. T
+ | ∃∃V,T. L ⊢ T ⇒ #i & T1 = 𝕗{Cast} V. T.
+#L #T1 #T2 #H elim H -H L T1 T2
+[ #L #k #i #H destruct
+| #L #j #i /2/
+| #L #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
+| #L #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
+| #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct
+| #L #K #V1 #V2 #V #j #HLK #HV12 #HV2 #_ #i #H destruct -V;
+ elim (lift_inv_lref2 … HV2) -HV2 * #H1 #H2
+ [ elim (lt_zero_false … H1)
+ | destruct -V2 /3 width=7/
+ ]
+| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #i #H destruct
+| #L #V #T #T1 #T2 #HT1 #HT12 #_ #i #H destruct /3 width=6/
+| #L #V #T1 #T2 #HT12 #_ #i #H destruct /3/
+]
+qed.
+
+lemma pr_inv_lref2: ∀L,T1,i. L ⊢ T1 ⇒ #i →
+ ∨∨ T1 = #i
+ | ∃∃K,V1,j. j < i & K ⊢ V1 ⇒ #(i-j-1) &
+ ↑[O,j] K. 𝕓{Abbr} V1 ≡ L & T1 = #j
+ | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & L ⊢ T0 ⇒ #i &
+ T1 = 𝕓{Abbr} V. T
+ | ∃∃V,T. L ⊢ T ⇒ #i & T1 = 𝕗{Cast} V. T.
+/2/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "lambda-delta/substitution/lift_fun.ma".
+include "lambda-delta/substitution/lift_main.ma".
+include "lambda-delta/substitution/drop_main.ma".
+include "lambda-delta/reduction/pr_defs.ma".
+
+lemma pr_lift: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → ∀d,e,K. ↑[d,e] L ≡ K →
+ ∀U1. ↑[d,e] T1 ≡ U1 → ∀U2. ↑[d,e] T2 ≡ U2 → K ⊢ U1 ⇒ U2.
+#L #T1 #T2 #H elim H -H L T1 T2
+[ #L #k #d #e #K #_ #U1 #HU1 #U2 #HU2
+ lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1;
+ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 //
+| #L #i #d #e #K #_ #U1 #HU1 #U2 #HU2
+ lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1;
+ lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 //
+| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2
+ elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
+ elim (lift_inv_bind1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2
+ /5 width=5/
+| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2
+ elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
+ elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2
+ /3 width=5/
+| #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2
+ elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
+ elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
+ elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2
+ /5 width=5/
+| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HKL #X #HX #V3 #HV03
+ lapply (lift_inv_lref1 … HX) -HX * * #Hid #H destruct -X;
+ [ -HV12;
+ elim (lift_trans_ge … HV20 … HV03 ?) -HV20 HV03 V0 // #V0 #HV20 #HV03
+ elim (drop_trans_le … HKL … HLK0 ?) -HKL HLK0 L /2/ #L #HKL #HLK0
+ elim (drop_inv_skip2 … HLK0 ?) -HLK0 /2/ #K1 #V #HK10 #HV #H destruct -L;
+ @pr_delta [4,6: // |1,2,3: skip |5: /2 width=5/] (**) (* /2 width=5/ *)
+ | -IHV12;
+ lapply (lift_trans_be … HV20 … HV03 ? ?) -HV20 HV03 V0 /2/ #HV23
+ lapply (drop_trans_ge … HKL … HLK0 ?) -HKL HLK0 L // -Hid #HKK0
+ @pr_delta /width=6/
+ ]
+| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2
+ elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
+ elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
+ elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2;
+ elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X;
+ lapply (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // * #V #HV2 #HV3
+ @pr_theta /3 width=5/
+| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HKL #X #HX #T0 #HT20
+ elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X;
+ lapply (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // * #T #HT1 #HT3
+ @pr_zeta [2: // |1:skip | /2 width=5/] (**) (* /2 width=5/ *)
+| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HKL #X #HX #T #HT2
+ elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X;
+ @pr_tau /2 width=5/
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "lambda-delta/substitution/lift_main.ma".
+include "lambda-delta/substitution/subst_defs.ma".
+include "lambda-delta/reduction/pr_defs.ma".
+
+lemma subst_pr: ∀d,e,L,T1,U2. L ⊢ ↓[d,e] T1 ≡ U2 → ∀T2. ↑[d,e] U2 ≡ T2 →
+ L ⊢ T1 ⇒ T2.
+#d #e #L #T1 #U2 #H elim H -H d e L T1 U2
+[ #L #k #d #e #X #HX
+ lapply (lift_inv_sort1 … HX) -HX #HX destruct -X //
+| #L #i #d #e #Hid #X #HX
+ lapply (lift_inv_lref1_lt … HX Hid) -HX #HX destruct -X //
+| #L #K #V #U1 #U2 #i #d #e #Hdi #Hide #HLK #_ #HU12 #IHVU1 #U #HU2
+ lapply (lift_trans_be … HU12 … HU2 ? ?) // -HU12 HU2 U2 #HU1
+ elim (lift_free … HU1 0 (d+e-i-1) ? ? ?) -HU1 // #U2 #HU12 >arith6 // #HU2
+ @pr_delta [4,5,6: /2/ |1,2,3: skip ] (**) (* /2/ *)
+| #L #i #d #e #Hdei #X #HX
+ lapply (lift_inv_lref1_ge … HX ?) -HX /2/ #HX destruct -X;
+ >arith7 /2/
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
+ elim (lift_inv_bind1 … HX) -HX #V #T #HV2 #HT2 #HX destruct -X /3/
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
+ elim (lift_inv_flat1 … HX) -HX #V #T #HV2 #HT2 #HX destruct -X /3/
+]
+qed.
+(*
+lemma pr_subst_pr: ∀L,T1,T. L ⊢ T1 ⇒ T → ∀d,e,U. L ⊢ ↓[d,e] T ≡ U →
+ ∀T2. ↑[d,e] U ≡ T2 → L ⊢ T1 ⇒ T2.
+#L #T1 #T #H elim H -H L T1 T
+[ /2 width=5/
+| /2 width=5/
+| #L #I #V1 #V2 #T1 #T2 #HV12 #HT12 #IHV12 #IHT12 #d #e #X2 #HX2 #X1 #HX1
+ elim (subst_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #H destruct -X2;
+ elim (lift_inv_bind1 … HX1) -HX1 #V4 #T4 #HV34 #HT34 #H destruct -X1;
+ @pr_bind /2 width=5/ @IHT12
+| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X2 #HX2 #X1 #HX1
+ elim (subst_inv_flat1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #H destruct -X2;
+ elim (lift_inv_flat1 … HX1) -HX1 #V4 #T4 #HV34 #HT34 #H destruct -X1;
+ /3 width=5/
+| #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X2 #HX2 #X1 #HX1
+ elim (subst_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #H destruct -X2;
+ elim (lift_inv_bind1 … HX1) -HX1 #V4 #T4 #HV34 #HT34 #H destruct -X1;
+ @pr_beta /2 width=5/ @IHT12
+| #L #K #V1 #V2 #V #i #HLK #HV12 #HV2 #IHV12 #d #e #U #HVU #U0 #HU0
+ lapply (lift_free … HU0 0 (i + 1 + e) ? ? ?) //
+
+
+ @pr_delta [4: // |1,2: skip |6:
+*)
↑[d - 1, e] V2 ≡ V1 &
L1 = K1. 𝕓{I} V1.
#d #e #L1 #L2 #H elim H -H d e L1 L2
-[ #L #H elim (lt_false … H)
-| #L1 #L2 #I #V #e #_ #_ #H elim (lt_false … H)
+[ #L #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V #e #_ #_ #H elim (lt_refl_false … H)
| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #_ #I #L2 #V2 #H destruct -X Y Z;
/2 width=5/
]
lemma lift_inv_lref1_lt: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → i < d → T2 = #i.
#d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * //
#Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd
-elim (lt_false … Hdd)
+elim (lt_refl_false … Hdd)
qed.
lemma lift_inv_lref1_ge: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → d ≤ i → T2 = #(i + e).
#d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * //
#Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd
-elim (lt_false … Hdd)
+elim (lt_refl_false … Hdd)
qed.
lemma lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
inductive subst: lenv → term → nat → nat → term → Prop ≝
| subst_sort : ∀L,k,d,e. subst L (⋆k) d e (⋆k)
| subst_lref_lt: ∀L,i,d,e. i < d → subst L (#i) d e (#i)
-| subst_lref_be: ∀L,K,V,U,i,d,e.
+| subst_lref_be: ∀L,K,V,U1,U2,i,d,e.
d ≤ i → i < d + e →
- ↑[0, i] K. 𝕓{Abbr} V ≡ L → subst K V d (d + e - i - 1) U →
- subst L (#i) d e U
+ ↑[0, i] K. 𝕓{Abbr} V ≡ L → subst K V 0 (d + e - i - 1) U1 →
+ ↑[0, d] U1 ≡ U2 → subst L (#i) d e U2
| subst_lref_ge: ∀L,i,d,e. d + e ≤ i → subst L (#i) d e (#(i - e))
| subst_bind : ∀L,I,V1,V2,T1,T2,d,e.
subst L V1 d e V2 → subst (L. 𝕓{I} V1) T1 (d + 1) e T2 →
interpretation "telescopic substritution" 'RSubst L T1 d e T2 = (subst L T1 d e T2).
+(* The basic properties *****************************************************)
+
+lemma subst_lift_inv: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀L. L ⊢ ↓[d,e] T2 ≡ T1.
+#d #e #T1 #T2 #H elim H -H d e T1 T2 /2/
+#i #d #e #Hdi #L >(minus_plus_m_m i e) in ⊢ (? ? ? ? ? %) /3/
+qed.
+(*
+| subst_lref_O : ∀L,V1,V2,e. subst L V1 0 e V2 →
+ subst (L. 𝕓{Abbr} V1) #0 0 (e + 1) V2
+| subst_lref_S : ∀L,I,V,i,T1,T2,d,e.
+ d ≤ i → i < d + e → subst L #i d e T1 → ↑[d,1] T2 ≡ T1 →
+ subst (L. 𝕓{I} V) #(i + 1) (d + 1) e T2
+*)
(* The basic inversion lemmas ***********************************************)
+lemma subst_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ ↓[d, e] U1 ≡ U2 →
+ ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
+ ∃∃V2,T2. subst L V1 d e V2 &
+ subst (L. 𝕓{I} V1) T1 (d + 1) e T2 &
+ U2 = 𝕓{I} V2. T2.
+#d #e #L #U1 #U2 #H elim H -H d e L U1 U2
+[ #L #k #d #e #I #V1 #T1 #H destruct
+| #L #i #d #e #_ #I #V1 #T1 #H destruct
+| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
+| #L #i #d #e #_ #I #V1 #T1 #H destruct
+| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/
+| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct
+]
+qed.
+
+lemma subst_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ↓[d, e] 𝕓{I} V1. T1 ≡ U2 →
+ ∃∃V2,T2. subst L V1 d e V2 &
+ subst (L. 𝕓{I} V1) T1 (d + 1) e T2 &
+ U2 = 𝕓{I} V2. T2.
+/2/ qed.
+
+lemma subst_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ ↓[d, e] U1 ≡ U2 →
+ ∀I,V1,T1. U1 = 𝕗{I} V1. T1 →
+ ∃∃V2,T2. subst L V1 d e V2 & subst L T1 d e T2 &
+ U2 = 𝕗{I} V2. T2.
+#d #e #L #U1 #U2 #H elim H -H d e L U1 U2
+[ #L #k #d #e #I #V1 #T1 #H destruct
+| #L #i #d #e #_ #I #V1 #T1 #H destruct
+| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
+| #L #i #d #e #_ #I #V1 #T1 #H destruct
+| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct
+| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/
+]
+qed.
+
+lemma subst_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ ↓[d, e] 𝕗{I} V1. T1 ≡ U2 →
+ ∃∃V2,T2. subst L V1 d e V2 & subst L T1 d e T2 &
+ U2 = 𝕗{I} V2. T2.
+/2/ qed.
+(*
lemma subst_inv_lref1_be_aux: ∀d,e,L,T,U. L ⊢ ↓[d, e] T ≡ U →
∀i. d ≤ i → i < d + e → T = #i →
∃∃K,V. ↑[0, i] K. 𝕓{Abbr} V ≡ L &
∃∃K,V. ↑[0, i] K. 𝕓{Abbr} V ≡ L &
K ⊢ ↓[d, d + e - i - 1] V ≡ U.
/2/ qed.
-
-(* The basic properties *****************************************************)
-
-lemma subst_lift_inv: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀L. L ⊢ ↓[d,e] T2 ≡ T1.
-#d #e #T1 #T2 #H elim H -H d e T1 T2 /2/
-#i #d #e #Hdi #L >(minus_plus_m_m i e) in ⊢ (? ? ? ? ? %) /3/
-qed.
-(*
-| subst_lref_O : ∀L,V1,V2,e. subst L V1 0 e V2 →
- subst (L. 𝕓{Abbr} V1) #0 0 (e + 1) V2
-| subst_lref_S : ∀L,I,V,i,T1,T2,d,e.
- d ≤ i → i < d + e → subst L #i d e T1 → ↑[d,1] T2 ≡ T1 →
- subst (L. 𝕓{I} V) #(i + 1) (d + 1) e T2
*)
K1 ⊢ ↓[d - 1, e] V1 ≡ V2 &
L1 = K1. 𝕓{I} V1.
#d #e #L1 #L2 #H elim H -H d e L1 L2
-[ #L #H elim (lt_false … H)
-| #L1 #L2 #I #V #e #_ #_ #H elim (lt_false … H)
+[ #L #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V #e #_ #_ #H elim (lt_refl_false … H)
| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #_ #I #L2 #V2 #H destruct -X Y Z;
/2 width=5/
]
interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2).
+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).
+
+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 or4 (P0,P1,P2,P3:Prop) : Prop ≝
+ | or4_intro0: P0 → or4 ? ? ? ?
+ | or4_intro1: P1 → or4 ? ? ? ?
+ | or4_intro2: P2 → or4 ? ? ? ?
+ | or4_intro3: P3 → or4 ? ? ? ?
+.
+
+interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3).
+
(* This file was generated by xoa.native: do not edit *********************)
-notation "hvbox(∃∃ ident x0 . term 19 P0 & term 19 P1)"
+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 . term 19 P0 & term 19 P1)"
+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 . term 19 P0 & term 19 P1 & 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}.$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)"
+ 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(∨∨ term 19 P0 break | term 19 P1 break | term 19 P2 break | term 19 P3)"
+ non associative with precedence 20
+ for @{ 'Or $P0 $P1 $P2 $P3 }.
+
projects / helm.git / commitdiff