update in ground, basic_2A and apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma
index 7ae7099b6e79685bcf2ef1c995b6f294ff2bb369..ff8a0164cc7d9e3b337afe638a4cacba3c39f909 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma
@@ -12,17 +12,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/relocation/mr2_at.ma".
-include "ground_2/relocation/mr2_plus.ma".
+include "ground/relocation/mr2_at.ma".
+include "ground/relocation/mr2_plus.ma".
 include "basic_2A/notation/relations/rliftstar_3.ma".
 include "basic_2A/substitution/lift.ma".
 
 (* GENERIC TERM RELOCATION **************************************************)
 
 inductive lifts: mr2 → relation term ≝
-| lifts_nil : ∀T. lifts (◊) T T
+| lifts_nil : ∀T. lifts (𝐞) T T
 | lifts_cons: ∀T1,T,T2,cs,l,m.
-              ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts (❨l, m❩; cs) T1 T2
+              ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts (❨l, m❩◗ cs) T1 T2
 .
 
 interpretation "generic relocation (term)"
@@ -30,16 +30,16 @@ interpretation "generic relocation (term)"
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lifts_inv_nil_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → cs = ◊ → T1 = T2.
+fact lifts_inv_nil_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → cs = 𝐞 → T1 = T2.
 #T1 #T2 #cs * -T1 -T2 -cs //
 #T1 #T #T2 #l #m #cs #_ #_ #H destruct
 qed-.
 
-lemma lifts_inv_nil: ∀T1,T2. ⬆*[◊] T1 ≡ T2 → T1 = T2.
+lemma lifts_inv_nil: ∀T1,T2. ⬆*[𝐞] T1 ≡ T2 → T1 = T2.
 /2 width=3 by lifts_inv_nil_aux/ qed-.
 
 fact lifts_inv_cons_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 →
-                         ∀l,m,tl. cs = ❨l, m❩; tl →
+                         ∀l,m,tl. cs = ❨l, m❩◗ tl →
                          ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[tl] T ≡ T2.
 #T1 #T2 #cs * -T1 -T2 -cs
 [ #T #l #m #tl #H destruct
@@ -47,11 +47,10 @@ fact lifts_inv_cons_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 →
   /2 width=3 by ex2_intro/
 qed-.
 
-lemma lifts_inv_cons: ∀T1,T2,l,m,cs. ⬆*[❨l, m❩; cs] T1 ≡ T2 →
+lemma lifts_inv_cons: ∀T1,T2,l,m,cs. ⬆*[❨l, m❩◗ cs] T1 ≡ T2 →
                       ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[cs] T ≡ T2.
 /2 width=3 by lifts_inv_cons_aux/ qed-.
 
-(* Basic_1: was: lift1_sort *)
 lemma lifts_inv_sort1: ∀T2,k,cs. ⬆*[cs] ⋆k ≡ T2 → T2 = ⋆k.
 #T2 #k #cs elim cs -cs
 [ #H <(lifts_inv_nil … H) -H //
@@ -61,7 +60,6 @@ lemma lifts_inv_sort1: ∀T2,k,cs. ⬆*[cs] ⋆k ≡ T2 → T2 = ⋆k.
 ]
 qed-.
 
-(* Basic_1: was: lift1_lref *)
 lemma lifts_inv_lref1: ∀T2,cs,i1. ⬆*[cs] #i1 ≡ T2 →
                        ∃∃i2. @❪i1, cs❫ ≘ i2 & T2 = #i2.
 #T2 #cs elim cs -cs
@@ -82,7 +80,6 @@ lemma lifts_inv_gref1: ∀T2,p,cs. ⬆*[cs] §p ≡ T2 → T2 = §p.
 ]
 qed-.
 
-(* Basic_1: was: lift1_bind *)
 lemma lifts_inv_bind1: ∀a,I,T2,cs,V1,U1. ⬆*[cs] ⓑ{a,I} V1. U1 ≡ T2 →
                        ∃∃V2,U2. ⬆*[cs] V1 ≡ V2 & ⬆*[cs + 1] U1 ≡ U2 &
                                 T2 = ⓑ{a,I} V2. U2.
@@ -97,7 +94,6 @@ lemma lifts_inv_bind1: ∀a,I,T2,cs,V1,U1. ⬆*[cs] ⓑ{a,I} V1. U1 ≡ T2 →
 ]
 qed-.
 
-(* Basic_1: was: lift1_flat *)
 lemma lifts_inv_flat1: ∀I,T2,cs,V1,U1. ⬆*[cs] ⓕ{I} V1. U1 ≡ T2 →
                        ∃∃V2,U2. ⬆*[cs] V1 ≡ V2 & ⬆*[cs] U1 ≡ U2 &
                                 T2 = ⓕ{I} V2. U2.