From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 11 May 2014 20:15:34 +0000 (+0000)
Subject: advances on ldrop ....
X-Git-Tag: make_still_working~924
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3325b784763ae9e6bac4307463071bb38e5641c9

advances on ldrop ....
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
index 4263c55cd..9a5b0cc91 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
@@ -48,7 +48,7 @@ lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2,
 | #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
   /2 width=4 by fqu_flat_dx, ex3_intro/
 | #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1
-  elim (ldrop_O1_le (e+1) K1)
+  elim (ldrop_O1_le (Ⓕ) (e+1) K1)
   [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
     #H2KL elim (lpxs_ldrop_trans_O1 … H1KL1 … HL1) -L1
     #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma
index 7dc0b2a85..843bea88b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma
@@ -48,7 +48,7 @@ theorem csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀d. G ⊢ ⬊*[
 [ #i #HG #HL #HT #H #d destruct
   elim (lt_or_ge i (|L|)) /2 width=1 by lsx_lref_free/
   elim (ylt_split i d) /2 width=1 by lsx_lref_skip/
-  #Hdi #Hi elim (ldrop_O1_lt … Hi) -Hi
+  #Hdi #Hi elim (ldrop_O1_lt (Ⓕ) … Hi) -Hi
   #I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H
   /4 width=6 by lsx_lref_be, fqup_lref/
 | #a #I #V #T #HG #HL #HT #H #d destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc
index 888f83ef4..5a87c0da3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc
@@ -15,104 +15,6 @@
 include "basic_2/substitution/cofrees_lift.ma".
 include "basic_2/substitution/llpx_sn_alt1.ma".
 
-lemma le_plus_xSy_O_false: ∀x,y. x + S y ≤ 0 → ⊥.
-#x #y #H lapply (le_n_O_to_eq … H) -H <plus_n_Sm #H destruct
-qed-.
-
-lemma ldrop_fwd_length_ge: ∀L1,L2,d,e,s. ⇩[s, d, e] L1 ≡ L2 → |L1| ≤ d → |L2| = |L1|.
-#L1 #L2 #d #e #s #H elim H -L1 -L2 -d -e // normalize
-[ #I #L1 #L2 #V #e #_ #_ #H elim (le_plus_xSy_O_false … H)
-| /4 width=2 by le_plus_to_le_r, eq_f/
-]
-qed-.
-
-lemma ldrop_fwd_length_le_le: ∀L1,L2,d,e,s. ⇩[s, d, e] L1 ≡ L2 → d ≤ |L1| → e ≤ |L1| - d → |L2| = |L1| - e.
-#L1 #L2 #d #e #s #H elim H -L1 -L2 -d -e // normalize
-[ /3 width=2 by le_plus_to_le_r/
-| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #IHL12 >minus_plus_plus_l
-  #Hd #He lapply (le_plus_to_le_r … Hd) -Hd
-  #Hd >IHL12 // -L2 >plus_minus /2 width=3 by transitive_le/
-]
-qed-.
-
-lemma ldrop_fwd_length_le_ge: ∀L1,L2,d,e,s. ⇩[s, d, e] L1 ≡ L2 → d ≤ |L1| → |L1| - d ≤ e → |L2| = d.
-#L1 #L2 #d #e #s #H elim H -L1 -L2 -d -e normalize
-[ /2 width=1 by le_n_O_to_eq/
-| #I #L #V #_ <minus_n_O #H elim (le_plus_xSy_O_false … H)
-| /3 width=2 by le_plus_to_le_r/
-| /4 width=2 by le_plus_to_le_r, eq_f/
-]
-qed-.
-
-lemma ldrop_O1_le: ∀s,e,L. e ≤ |L| → ∃K. ⇩[s, 0, e] L ≡ K.
-#s #e @(nat_ind_plus … e) -e /2 width=2 by ex_intro/
-#e #IHe *
-[ #H elim (le_plus_xSy_O_false … H)
-| #L #I #V normalize #H elim (IHe L) -IHe /3 width=2 by ldrop_drop, monotonic_pred, ex_intro/
-]
-qed-.
-
-lemma ldrop_O1_lt: ∀s,L,e. e < |L| → ∃∃I,K,V. ⇩[s, 0, e] L ≡ K.ⓑ{I}V.
-#s #L elim L -L
-[ #e #H elim (lt_zero_false … H)
-| #L #I #V #IHL #e @(nat_ind_plus … e) -e /2 width=4 by ldrop_pair, ex1_3_intro/
-  #e #_ normalize #H elim (IHL e) -IHL /3 width=4 by ldrop_drop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/
-]
-qed-.
-
-lemma ldrop_O1_pair: ∀L,K,e,s. ⇩[s, 0, e] L ≡ K → e ≤ |L| → ∀I,V.
-                     ∃∃J,W. ⇩[s, 0, e] L.ⓑ{I}V ≡ K.ⓑ{J}W.
-#L elim L -L [| #L #Z #X #IHL ] #K #e #s #H normalize #He #I #V
-[ elim (ldrop_inv_atom1 … H) -H #H <(le_n_O_to_eq … He) -e
-  #Hs destruct /2 width=3 by ex1_2_intro/
-| elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK destruct /2 width=3 by ex1_2_intro/
-  elim (IHL … HLK … Z X) -IHL -HLK
-  /3 width=3 by ldrop_drop_lt, le_plus_to_minus, ex1_2_intro/
-]
-qed-.
-
-lemma ldrop_inv_O1_gt: ∀L,K,e,s. ⇩[s, 0, e] L ≡ K → |L| < e →
-                       s = Ⓣ ∧ K = ⋆.
-#L elim L -L [| #L #Z #X #IHL ] #K #e #s #H normalize in ⊢ (?%?→?); #H1e
-[ elim (ldrop_inv_atom1 … H) -H elim s -s /2 width=1 by conj/
-  #_ #Hs lapply (Hs ?) // -Hs #H destruct elim (lt_zero_false … H1e)
-| elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HLK destruct
-  [ elim (lt_zero_false … H1e)
-  | elim (IHL … HLK) -IHL -HLK /2 width=1 by lt_plus_to_minus_r, conj/
-  ]
-]
-qed-.
-
-lemma ldrop_O1_ge: ∀L,e. |L| ≤ e → ⇩[Ⓣ, 0, e] L ≡ ⋆.
-#L elim L -L [ #e #_ @ldrop_atom #H destruct ]
-#L #I #V #IHL #e @(nat_ind_plus … e) -e [ #H elim (le_plus_xSy_O_false … H) ]
-normalize /4 width=1 by ldrop_drop, monotonic_pred/
-qed.
-
-lemma ldrop_split: ∀L1,L2,d,e2,s. ⇩[s, d, e2] L1 ≡ L2 → ∀e1. e1 ≤ e2 →
-                   ∃∃L. ⇩[s, d, e2 - e1] L1 ≡ L & ⇩[s, d, e1] L ≡ L2.
-#L1 #L2 #d #e2 #s #H elim H -L1 -L2 -d -e2
-[ #d #e2 #Hs #e1 #He12 @(ex2_intro … (⋆))
-  @ldrop_atom #H lapply (Hs H) -s #H destruct /2 width=1 by le_n_O_to_eq/
-| #I #L1 #V #e1 #He1 lapply (le_n_O_to_eq … He1) -He1
-  #H destruct /2 width=3 by ex2_intro/
-| #I #L1 #L2 #V #e2 #HL12 #IHL12 #e1 @(nat_ind_plus … e1) -e1
-  [ /3 width=3 by ldrop_drop, ex2_intro/
-  | -HL12 #e1 #_ #He12 lapply (le_plus_to_le_r … He12) -He12
-    #He12 elim (IHL12 … He12) -IHL12 >minus_plus_plus_l
-    #L #HL1 #HL2 elim (lt_or_ge (|L1|) (e2-e1)) #H0
-    [ elim (ldrop_inv_O1_gt … HL1 H0) -HL1 #H1 #H2 destruct
-      elim (ldrop_inv_atom1 … HL2) -HL2 #H #_ destruct
-      @(ex2_intro … (⋆)) [ @ldrop_O1_ge normalize // ]
-      @ldrop_atom #H destruct
-    | elim (ldrop_O1_pair … HL1 H0 I V) -HL1 -H0 /3 width=5 by ldrop_drop, ex2_intro/
-    ]
-  ]
-| #I #L1 #L2 #V1 #V2 #d #e2 #_ #HV21 #IHL12 #e1 #He12 elim (IHL12 … He12) -IHL12
-  #L #HL1 #HL2 elim (lift_split … HV21 d e1) -HV21 /3 width=5 by ldrop_skip, ex2_intro/
-]
-qed-.
-
 (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
 
 (* alternative definition of llpx_sn (not recursive) *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma
index 3ff9a954f..ad6e23ee7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma
@@ -43,7 +43,7 @@ lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2,
 | #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
   /2 width=4 by fqu_flat_dx, ex3_intro/
 | #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1
-  elim (ldrop_O1_le (e+1) K1)
+  elim (ldrop_O1_le (Ⓕ) (e+1) K1)
   [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
     #H2KL elim (lpx_ldrop_trans_O1 … H1KL1 … HL1) -L1
     #K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/gget.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/gget.ma
index 5ef11dc4b..f299c9bea 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/gget.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/gget.ma
@@ -30,7 +30,7 @@ interpretation "global reading"
 
 lemma gget_inv_gt: ∀G1,G2,e. ⇩[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
 #G1 #G2 #e * -G1 -G2 //
-[ #G #H >H -H >commutative_plus #H
+[ #G #H >H -H >commutative_plus #H (**) (* lemma needed here *)
   lapply (le_plus_to_le_r … 0 H) -H #H
   lapply (le_n_O_to_eq … H) -H #H destruct
 | #I #G1 #G2 #V #H1 #_ #H2
@@ -42,7 +42,7 @@ qed-.
 
 lemma gget_inv_eq: ∀G1,G2,e. ⇩[e] G1 ≡ G2 → |G1| = e + 1 → G1 = G2.
 #G1 #G2 #e * -G1 -G2 //
-[ #G #H1 #H2 >H2 in H1; -H2 >commutative_plus #H
+[ #G #H1 #H2 >H2 in H1; -H2 >commutative_plus #H (**) (* lemma needed here *)
   lapply (le_plus_to_le_r … 0 H) -H #H
   lapply (le_n_O_to_eq … H) -H #H destruct
 | #I #G1 #G2 #V #H1 #_ normalize #H2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
index 80be988b0..0b1f18ba4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
@@ -166,6 +166,18 @@ lemma ldrop_inv_skip2: ∀I,L1,K2,V2,s,d,e. ⇩[s, d, e] L1 ≡ K2.ⓑ{I}V2 →
                                 L1 = K1.ⓑ{I}V1.
 /2 width=3 by ldrop_inv_skip2_aux/ qed-.
 
+lemma ldrop_inv_O1_gt: ∀L,K,e,s. ⇩[s, 0, e] L ≡ K → |L| < e →
+                       s = Ⓣ ∧ K = ⋆.
+#L elim L -L [| #L #Z #X #IHL ] #K #e #s #H normalize in ⊢ (?%?→?); #H1e
+[ elim (ldrop_inv_atom1 … H) -H elim s -s /2 width=1 by conj/
+  #_ #Hs lapply (Hs ?) // -Hs #H destruct elim (lt_zero_false … H1e)
+| elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HLK destruct
+  [ elim (lt_zero_false … H1e)
+  | elim (IHL … HLK) -IHL -HLK /2 width=1 by lt_plus_to_minus_r, conj/
+  ]
+]
+qed-.
+
 (* Basic properties *********************************************************)
 
 lemma ldrop_refl_atom_O2: ∀s,d. ⇩[s, d, O] ⋆ ≡ ⋆.
@@ -188,21 +200,60 @@ lemma ldrop_skip_lt: ∀I,L1,L2,V1,V2,s,d,e.
 #I #L1 #L2 #V1 #V2 #s #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) /2 width=1 by ldrop_skip/
 qed.
 
-lemma ldrop_O1_le: ∀e,L. e ≤ |L| → ∃K. ⇩[e] L ≡ K.
-#e @(nat_ind_plus … e) -e /2 width=2 by ex_intro/
+lemma ldrop_O1_le: ∀s,e,L. e ≤ |L| → ∃K. ⇩[s, 0, e] L ≡ K.
+#s #e @(nat_ind_plus … e) -e /2 width=2 by ex_intro/
 #e #IHe *
-[ #H lapply (le_n_O_to_eq … H) -H >commutative_plus normalize #H destruct
-| #L #I #V normalize #H
-  elim (IHe L) -IHe /3 width=2 by ldrop_drop, monotonic_pred, ex_intro/
+[ #H elim (le_plus_xSy_O_false … H)
+| #L #I #V normalize #H elim (IHe L) -IHe /3 width=2 by ldrop_drop, monotonic_pred, ex_intro/
 ]
 qed-.
 
-lemma ldrop_O1_lt: ∀L,e. e < |L| → ∃∃I,K,V. ⇩[e] L ≡ K.ⓑ{I}V.
-#L elim L -L
+lemma ldrop_O1_lt: ∀s,L,e. e < |L| → ∃∃I,K,V. ⇩[s, 0, e] L ≡ K.ⓑ{I}V.
+#s #L elim L -L
 [ #e #H elim (lt_zero_false … H)
 | #L #I #V #IHL #e @(nat_ind_plus … e) -e /2 width=4 by ldrop_pair, ex1_3_intro/
-  #e #_ normalize #H
-  elim (IHL e) -IHL /3 width=4 by ldrop_drop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/
+  #e #_ normalize #H elim (IHL e) -IHL /3 width=4 by ldrop_drop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/
+]
+qed-.
+
+lemma ldrop_O1_pair: ∀L,K,e,s. ⇩[s, 0, e] L ≡ K → e ≤ |L| → ∀I,V.
+                     ∃∃J,W. ⇩[s, 0, e] L.ⓑ{I}V ≡ K.ⓑ{J}W.
+#L elim L -L [| #L #Z #X #IHL ] #K #e #s #H normalize #He #I #V
+[ elim (ldrop_inv_atom1 … H) -H #H <(le_n_O_to_eq … He) -e
+  #Hs destruct /2 width=3 by ex1_2_intro/
+| elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK destruct /2 width=3 by ex1_2_intro/
+  elim (IHL … HLK … Z X) -IHL -HLK
+  /3 width=3 by ldrop_drop_lt, le_plus_to_minus, ex1_2_intro/
+]
+qed-.
+
+lemma ldrop_O1_ge: ∀L,e. |L| ≤ e → ⇩[Ⓣ, 0, e] L ≡ ⋆.
+#L elim L -L [ #e #_ @ldrop_atom #H destruct ]
+#L #I #V #IHL #e @(nat_ind_plus … e) -e [ #H elim (le_plus_xSy_O_false … H) ]
+normalize /4 width=1 by ldrop_drop, monotonic_pred/
+qed.
+
+lemma ldrop_split: ∀L1,L2,d,e2,s. ⇩[s, d, e2] L1 ≡ L2 → ∀e1. e1 ≤ e2 →
+                   ∃∃L. ⇩[s, d, e2 - e1] L1 ≡ L & ⇩[s, d, e1] L ≡ L2.
+#L1 #L2 #d #e2 #s #H elim H -L1 -L2 -d -e2
+[ #d #e2 #Hs #e1 #He12 @(ex2_intro … (⋆))
+  @ldrop_atom #H lapply (Hs H) -s #H destruct /2 width=1 by le_n_O_to_eq/
+| #I #L1 #V #e1 #He1 lapply (le_n_O_to_eq … He1) -He1
+  #H destruct /2 width=3 by ex2_intro/
+| #I #L1 #L2 #V #e2 #HL12 #IHL12 #e1 @(nat_ind_plus … e1) -e1
+  [ /3 width=3 by ldrop_drop, ex2_intro/
+  | -HL12 #e1 #_ #He12 lapply (le_plus_to_le_r … He12) -He12
+    #He12 elim (IHL12 … He12) -IHL12 >minus_plus_plus_l
+    #L #HL1 #HL2 elim (lt_or_ge (|L1|) (e2-e1)) #H0
+    [ elim (ldrop_inv_O1_gt … HL1 H0) -HL1 #H1 #H2 destruct
+      elim (ldrop_inv_atom1 … HL2) -HL2 #H #_ destruct
+      @(ex2_intro … (⋆)) [ @ldrop_O1_ge normalize // ]
+      @ldrop_atom #H destruct
+    | elim (ldrop_O1_pair … HL1 H0 I V) -HL1 -H0 /3 width=5 by ldrop_drop, ex2_intro/
+    ]
+  ]
+| #I #L1 #L2 #V1 #V2 #d #e2 #_ #HV21 #IHL12 #e1 #He12 elim (IHL12 … He12) -IHL12
+  #L #HL1 #HL2 elim (lift_split … HV21 d e1) -HV21 /3 width=5 by ldrop_skip, ex2_intro/
 ]
 qed-.
 
@@ -281,6 +332,31 @@ lemma ldrop_fwd_drop2: ∀L1,I2,K2,V2,s,e. ⇩[s, O, e] L1 ≡ K2. ⓑ{I2} V2 
 ]
 qed-.
 
+lemma ldrop_fwd_length_ge: ∀L1,L2,d,e,s. ⇩[s, d, e] L1 ≡ L2 → |L1| ≤ d → |L2| = |L1|.
+#L1 #L2 #d #e #s #H elim H -L1 -L2 -d -e // normalize
+[ #I #L1 #L2 #V #e #_ #_ #H elim (le_plus_xSy_O_false … H)
+| /4 width=2 by le_plus_to_le_r, eq_f/
+]
+qed-.
+
+lemma ldrop_fwd_length_le_le: ∀L1,L2,d,e,s. ⇩[s, d, e] L1 ≡ L2 → d ≤ |L1| → e ≤ |L1| - d → |L2| = |L1| - e.
+#L1 #L2 #d #e #s #H elim H -L1 -L2 -d -e // normalize
+[ /3 width=2 by le_plus_to_le_r/
+| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #IHL12 >minus_plus_plus_l
+  #Hd #He lapply (le_plus_to_le_r … Hd) -Hd
+  #Hd >IHL12 // -L2 >plus_minus /2 width=3 by transitive_le/
+]
+qed-.
+
+lemma ldrop_fwd_length_le_ge: ∀L1,L2,d,e,s. ⇩[s, d, e] L1 ≡ L2 → d ≤ |L1| → |L1| - d ≤ e → |L2| = d.
+#L1 #L2 #d #e #s #H elim H -L1 -L2 -d -e normalize
+[ /2 width=1 by le_n_O_to_eq/
+| #I #L #V #_ <minus_n_O #H elim (le_plus_xSy_O_false … H)
+| /3 width=2 by le_plus_to_le_r/
+| /4 width=2 by le_plus_to_le_r, eq_f/
+]
+qed-.
+
 lemma ldrop_fwd_length: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L1| = |L2| + e.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize /2 width=1 by/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma
index 77e7e5b59..ef59a2a3d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma
@@ -48,7 +48,7 @@ theorem ldrop_conf_ge: ∀L,L1,s1,d1,e1. ⇩[s1, d1, e1] L ≡ L1 →
 | #I #L #K #V1 #V2 #d #e #_ #_ #IHLK #L2 #s2 #e2 #H #Hdee2
   lapply (transitive_le 1 … Hdee2) // #He2
   lapply (ldrop_inv_drop1_lt … H ?) -H // -He2 #HL2
-  lapply (transitive_le (1 + e) … Hdee2) // #Hee2
+  lapply (transitive_le (1+e) … Hdee2) // #Hee2
   @ldrop_drop_lt >minus_minus_comm /3 width=1 by lt_minus_to_plus_r, monotonic_le_minus_r, monotonic_pred/ (**) (* explicit constructor *)
 ]
 qed.
@@ -201,7 +201,7 @@ qed-.
 
 lemma ldrop_fwd_be: ∀L,K,s,d,e,i. ⇩[s, d, e] L ≡ K → |K| ≤ i → i < d → |L| ≤ i.
 #L #K #s #d #e #i #HLK #HK #Hd elim (lt_or_ge i (|L|)) //
-#HL elim (ldrop_O1_lt … HL) #I #K0 #V #HLK0 -HL
+#HL elim (ldrop_O1_lt (Ⓕ) … HL) #I #K0 #V #HLK0 -HL
 elim (ldrop_conf_lt … HLK … HLK0) // -HLK -HLK0 -Hd
 #K1 #V1 #HK1 #_ #_ lapply (ldrop_fwd_length_lt2 … HK1) -I -K1 -V1
 #H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma
index 91b20e720..75586d3d3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma
@@ -63,7 +63,7 @@ lemma ldrop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i →
                    ∃∃L2. L1 ≃[0, i] L2 & ⇩[i] L2 ≡ K2.
 #K2 #i @(nat_ind_plus … i) -i
 [ /3 width=3 by leq_O2, ex2_intro/
-| #i #IHi #Y #Hi elim (ldrop_O1_lt Y 0) //
+| #i #IHi #Y #Hi elim (ldrop_O1_lt (Ⓕ) Y 0) //
   #I #L1 #V #H lapply (ldrop_inv_O2 … H) -H #H destruct
   normalize in Hi; elim (IHi L1) -IHi
   /3 width=5 by ldrop_drop, leq_pair, injective_plus_l, ex2_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
index eb2c7bfec..77bcf4c7a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
@@ -59,7 +59,7 @@ qed.
 
 lemma lsuby_O2: ∀L2,L1,d. |L2| ≤ |L1| → L1 ⊆[d, yinj 0] L2.
 #L2 elim L2 -L2 // #L2 #I2 #V2 #IHL2 * normalize
-[ #d #H lapply (le_n_O_to_eq … H) -H <plus_n_Sm #H destruct
+[ #d #H elim (le_plus_xSy_O_false … H)
 | #L1 #I1 #V1 #d #H lapply (le_plus_to_le_r … H) -H #HL12
  elim (ynat_cases d) /3 width=1 by lsuby_zero/
  * /3 width=1 by lsuby_succ/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
index 52759ca7f..c571d9991 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
@@ -103,7 +103,7 @@ theorem cpys_antisym_eq: ∀G,L1,T1,T2,d,e. ⦃G, L1⦄ ⊢ T1 ▶*[d, e] T2 →
     lapply (cpys_weak … HW2 0 (i+1) ? ?) -HW2 //
     [ >yplus_O1 >yplus_O1 /3 width=1 by ylt_fwd_le, ylt_inj/ ] -Hi
     #HW2 >(cpys_inv_lift1_eq … HW2) -HW2 //
-  | elim (ldrop_O1_le … Hi) -Hi #K2 #HLK2
+  | elim (ldrop_O1_le (Ⓕ) … Hi) -Hi #K2 #HLK2
     elim (cpys_inv_lift1_ge_up … HW2 … HLK2 … HVW2 ? ? ?) -HW2 -HLK2 -HVW2
     /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ -Hdi -Hide
     #X #_ #H elim (lift_inv_lref2_be … H) -H //
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma
index ac1329b45..c54215e60 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma
@@ -36,7 +36,7 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ 
 | #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H
   /2 width=3 by fqu_flat_dx, ex2_intro/
 | #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12
-  elim (ldrop_O1_le (e+1) L1)
+  elim (ldrop_O1_le (Ⓕ) (e+1) L1)
   [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
   | lapply (ldrop_fwd_length_le2 … HLK2) -K2
     lapply (lleq_fwd_length … HL12) -T -U //
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt1.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt1.ma
index 7e071f24d..18872b671 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt1.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt1.ma
@@ -107,8 +107,8 @@ lemma llpx_sn_alt1_fwd_lref: ∀R,L1,L2,d,i. llpx_sn_alt1 R d (#i) L1 L2 →
 #R #L1 #L2 #d #i #H elim (llpx_sn_alt1_inv_alt … H) -H
 #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=1 by or3_intro0, conj/
 elim (ylt_split i d) /3 width=1 by or3_intro1/
-#Hdi #HL1 elim (ldrop_O1_lt … HL1)
-#I1 #K1 #V1 #HLK1 elim (ldrop_O1_lt L2 i) //
+#Hdi #HL1 elim (ldrop_O1_lt (Ⓕ) … HL1)
+#I1 #K1 #V1 #HLK1 elim (ldrop_O1_lt (Ⓕ) L2 i) //
 #I2 #K2 #V2 #HLK2 elim (IH … HLK1 HLK2) -IH
 /3 width=9 by nlift_lref_be_SO, or3_intro2, ex5_5_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_ldrop.ma
index 04a0f9295..509a836b3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_ldrop.ma
@@ -134,8 +134,8 @@ lemma llpx_sn_dec: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) →
   [ #HL12 #d elim (ylt_split i d) /3 width=1 by llpx_sn_skip, or_introl/
     #Hdi elim (lt_or_ge i (|L1|)) #HiL1
     elim (lt_or_ge i (|L2|)) #HiL2 /3 width=1 by or_introl, llpx_sn_free/
-    elim (ldrop_O1_lt … HiL2) #I2 #K2 #V2 #HLK2
-    elim (ldrop_O1_lt … HiL1) #I1 #K1 #V1 #HLK1
+    elim (ldrop_O1_lt (Ⓕ) … HiL2) #I2 #K2 #V2 #HLK2
+    elim (ldrop_O1_lt (Ⓕ) … HiL1) #I1 #K1 #V1 #HLK1
     elim (eq_bind2_dec I2 I1)
     [ #H2 elim (HR I1 K1 V1 V2) -HR
       [ #H3 elim (IH K1 V1 … K2 0) destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_lpx_sn.ma
index 7486958ae..21a88ca0e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_lpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_lpx_sn.ma
@@ -28,7 +28,7 @@ lemma lpx_sn_llpx_sn: ∀R. (∀I,L. reflexive … (R I L)) →
   [2: -IH /4 width=4 by lpx_sn_fwd_length, llpx_sn_free, le_repl_sn_conf_aux/ ]
   #Hi #Hn #L2 #d elim (ylt_split i d) 
   [ -n /3 width=2 by llpx_sn_skip, lpx_sn_fwd_length/ ]
-  #Hdi #HL12 elim (ldrop_O1_lt L1 i) //
+  #Hdi #HL12 elim (ldrop_O1_lt (Ⓕ) L1 i) //
   #I #K1 #V1 #HLK1 elim (lpx_sn_ldrop_conf … HL12 … HLK1) -HL12
   /4 width=9 by llpx_sn_lref, ldrop_fwd_rfw/
 | -HR -IH /4 width=2 by lpx_sn_fwd_length, llpx_sn_gref/
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 92b07e1f2..3eec591c6 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -36,7 +36,7 @@ lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
 qed.
 
 lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
-#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/
+#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1 by arith_b1/
 qed.
 
 lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
@@ -44,7 +44,7 @@ lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
 
 lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
                 a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
-#a1 #a2 #b #c1 #H1 #H2 >plus_minus // /2 width=1/
+#a1 #a2 #b #c1 #H1 #H2 >plus_minus /2 width=1 by arith_b2/
 qed.
 
 lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
@@ -91,21 +91,21 @@ axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
 axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
 
 lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
-#m #n elim (lt_or_ge m n) /2 width=1/
-#H elim H -m /2 width=1/
-#m #Hm * #H /2 width=1/ /3 width=1/
+#m #n elim (lt_or_ge m n) /2 width=1 by or3_intro0/
+#H elim H -m /2 width=1 by or3_intro1/
+#m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/
 qed-.
 
 lemma lt_refl_false: ∀n. n < n → ⊥.
-#n #H elim (lt_to_not_eq … H) -H /2 width=1/
+#n #H elim (lt_to_not_eq … H) -H /2 width=1 by/
 qed-.
 
 lemma lt_zero_false: ∀n. n < 0 → ⊥.
-#n #H elim (lt_to_not_le … H) -H /2 width=1/
+#n #H elim (lt_to_not_le … H) -H /2 width=1 by/
 qed-.
 
 lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
-#x #y #H elim (decidable_lt x y) /2 width=1/
+#x #y #H elim (decidable_lt x y) /2 width=1 by not_lt_to_le/
 #Hxy elim (H Hxy)
 qed-.
 
@@ -113,12 +113,13 @@ lemma pred_inv_refl: ∀m. pred m = m → m = 0.
 * // normalize #m #H elim (lt_refl_false m) //
 qed-.
 
+lemma le_plus_xSy_O_false: ∀x,y. x + S y ≤ 0 → ⊥.
+#x #y #H lapply (le_n_O_to_eq … H) -H <plus_n_Sm #H destruct
+qed-.
+
 lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥.
-#y #z #x elim x -x
-[ #H lapply (le_n_O_to_eq … H) -H
-  <plus_n_Sm #H destruct
-| /3 width=1 by le_S_S_to_le/
-]
+#y #z #x elim x -x /3 width=1 by le_S_S_to_le/
+#H elim (le_plus_xSy_O_false … H)
 qed-.
 
 lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
@@ -162,7 +163,7 @@ let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝
 lemma tri_lt: ∀A,a1,a2,a3,n2,n1. n1 < n2 → tri A n1 n2 a1 a2 a3 = a1.
 #A #a1 #a2 #a3 #n2 elim n2 -n2
 [ #n1 #H elim (lt_zero_false … H)
-| #n2 #IH #n1 elim n1 -n1 // /3 width=1/
+| #n2 #IH #n1 elim n1 -n1 /3 width=1 by monotonic_lt_pred/
 ]
 qed.
 
@@ -173,6 +174,6 @@ qed.
 lemma tri_gt: ∀A,a1,a2,a3,n1,n2. n2 < n1 → tri A n1 n2 a1 a2 a3 = a3.
 #A #a1 #a2 #a3 #n1 elim n1 -n1
 [ #n2 #H elim (lt_zero_false … H)
-| #n1 #IH #n2 elim n2 -n2 // /3 width=1/
+| #n1 #IH #n2 elim n2 -n2 /3 width=1 by monotonic_lt_pred/
 ]
 qed.