From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 17 Jul 2011 18:33:56 +0000 (+0000)
Subject: more lemmas and some generated logical constants for them
X-Git-Tag: make_still_working~2364
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=b4d7d16ff7635d9430e92ba86eaf513a9ad9ff8e;p=helm.git

more lemmas and some generated logical constants for them
---

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index 87d8d9baf..23b028eb2 100644
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -34,14 +34,18 @@ lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
 #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.
@@ -58,3 +62,10 @@ lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
 
 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.
diff --git a/matita/matita/lib/lambda-delta/reduction/pr_defs.ma b/matita/matita/lib/lambda-delta/reduction/pr_defs.ma
index b8ddd5ace..b817d34ad 100644
--- a/matita/matita/lib/lambda-delta/reduction/pr_defs.ma
+++ b/matita/matita/lib/lambda-delta/reduction/pr_defs.ma
@@ -44,3 +44,38 @@ lemma pr_refl: ∀T,L. L ⊢ T ⇒ T.
 #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.
diff --git a/matita/matita/lib/lambda-delta/reduction/pr_lift.ma b/matita/matita/lib/lambda-delta/reduction/pr_lift.ma
new file mode 100644
index 000000000..9718bf870
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/reduction/pr_lift.ma
@@ -0,0 +1,69 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.
diff --git a/matita/matita/lib/lambda-delta/reduction/pr_subst.ma b/matita/matita/lib/lambda-delta/reduction/pr_subst.ma
new file mode 100644
index 000000000..c762091a5
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/reduction/pr_subst.ma
@@ -0,0 +1,62 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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: 
+*) 
diff --git a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
index 0644efdbe..3a827c3a0 100644
--- a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
+++ b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
@@ -32,8 +32,8 @@ lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↑[d, e] L2 ≡ L1 → 0 < d →
                                    ↑[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/
 ]
diff --git a/matita/matita/lib/lambda-delta/substitution/lift_defs.ma b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
index 1f9be7fe2..472aef809 100644
--- a/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
@@ -79,13 +79,13 @@ lemma lift_inv_lref1: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 →
 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 →
diff --git a/matita/matita/lib/lambda-delta/substitution/subst_defs.ma b/matita/matita/lib/lambda-delta/substitution/subst_defs.ma
index 27de6a5ce..c563157f4 100644
--- a/matita/matita/lib/lambda-delta/substitution/subst_defs.ma
+++ b/matita/matita/lib/lambda-delta/substitution/subst_defs.ma
@@ -16,10 +16,10 @@ include "lambda-delta/substitution/drop_defs.ma".
 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 →
@@ -31,8 +31,61 @@ inductive subst: lenv → term → nat → nat → term → Prop ≝
 
 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 &
@@ -56,17 +109,4 @@ lemma subst_inv_lref1_be: ∀d,e,i,L,U. L ⊢ ↓[d, e] #i ≡ U →
                           ∃∃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
 *)
diff --git a/matita/matita/lib/lambda-delta/substitution/thin_defs.ma b/matita/matita/lib/lambda-delta/substitution/thin_defs.ma
index 1e7847603..c8ef44925 100644
--- a/matita/matita/lib/lambda-delta/substitution/thin_defs.ma
+++ b/matita/matita/lib/lambda-delta/substitution/thin_defs.ma
@@ -31,8 +31,8 @@ lemma thin_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
                                    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/
 ]
diff --git a/matita/matita/lib/lambda-delta/xoa_defs.ma b/matita/matita/lib/lambda-delta/xoa_defs.ma
index 022c06607..38c434304 100644
--- a/matita/matita/lib/lambda-delta/xoa_defs.ma
+++ b/matita/matita/lib/lambda-delta/xoa_defs.ma
@@ -34,3 +34,24 @@ inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝
 
 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).
+
diff --git a/matita/matita/lib/lambda-delta/xoa_notation.ma b/matita/matita/lib/lambda-delta/xoa_notation.ma
index c16d28585..2e441f1cb 100644
--- a/matita/matita/lib/lambda-delta/xoa_notation.ma
+++ b/matita/matita/lib/lambda-delta/xoa_notation.ma
@@ -14,15 +14,27 @@
 
 (* 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 }.
+