update in ground, basic_2A and apps_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / multiple / drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops.ma
index 2e096edaf7900e036fa572a52c0eadda64f6c2b2..87f93c4f92941550c419de56b4f5cfacfe5841b8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/xoa/ex_4_3.ma".
-include "ground_2/relocation/mr2_minus.ma".
+include "ground/xoa/ex_4_3.ma".
+include "ground/relocation/mr2_minus.ma".
 include "basic_2A/notation/relations/rdropstar_3.ma".
 include "basic_2A/notation/relations/rdropstar_4.ma".
 include "basic_2A/substitution/drop.ma".
@@ -22,9 +22,9 @@ include "basic_2A/multiple/lifts_vector.ma".
 (* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)
 
 inductive drops (s:bool): mr2 → relation lenv ≝
-| drops_nil : ∀L. drops s (◊) L L
+| drops_nil : ∀L. drops s (𝐞) L L
 | drops_cons: ∀L1,L,L2,cs,l,m.
-              drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s (❨l, m❩; cs) L1 L2
+              drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s (❨l, m❩◗ cs) L1 L2
 .
 
 interpretation "iterated slicing (local environment) abstract"
@@ -49,17 +49,16 @@ definition d_liftables1_all: relation2 lenv term → predicate bool ≝
 
 (* Basic inversion lemmas ***************************************************)
 
-fact drops_inv_nil_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → cs = ◊ → L1 = L2.
+fact drops_inv_nil_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → cs = 𝐞 → L1 = L2.
 #L1 #L2 #s #cs * -L1 -L2 -cs //
 #L1 #L #L2 #l #m #cs #_ #_ #H destruct
 qed-.
 
-(* Basic_1: was: drop1_gen_pnil *)
-lemma drops_inv_nil: ∀L1,L2,s. ⬇*[s, ◊] L1 ≡ L2 → L1 = L2.
+lemma drops_inv_nil: ∀L1,L2,s. ⬇*[s, 𝐞] L1 ≡ L2 → L1 = L2.
 /2 width=4 by drops_inv_nil_aux/ qed-.
 
 fact drops_inv_cons_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 →
-                         ∀l,m,tl. cs = ❨l, m❩; tl →
+                         ∀l,m,tl. cs = ❨l, m❩◗ tl →
                          ∃∃L. ⬇*[s, tl] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
 #L1 #L2 #s #cs * -L1 -L2 -cs
 [ #L #l #m #tl #H destruct
@@ -68,8 +67,7 @@ fact drops_inv_cons_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 →
 ]
 qed-.
 
-(* Basic_1: was: drop1_gen_pcons *)
-lemma drops_inv_cons: ∀L1,L2,s,l,m,cs. ⬇*[s, ❨l, m❩; cs] L1 ≡ L2 →
+lemma drops_inv_cons: ∀L1,L2,s,l,m,cs. ⬇*[s, ❨l, m❩◗ cs] L1 ≡ L2 →
                       ∃∃L. ⬇*[s, cs] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
 /2 width=3 by drops_inv_cons_aux/ qed-.
 
@@ -96,7 +94,6 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-(* Basic_1: was: drop1_skip_bind *)
 lemma drops_skip: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → ∀V1,V2. ⬆*[cs] V2 ≡ V1 →
                   ∀I. ⬇*[s, cs + 1] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2.
 #L1 #L2 #s #cs #H elim H -L1 -L2 -cs
@@ -119,5 +116,3 @@ lemma d1_liftables_liftables_all: ∀R,s. d_liftables1 R s → d_liftables1_all
 #R #s #HR #L #K #cs #HLK #Ts #Us #H elim H -Ts -Us normalize //
 #Ts #Us #T #U #HTU #_ #IHTUs * /3 width=7 by conj/
 qed.
-
-(* Basic_1: removed theorems 1: drop1_getl_trans *)