X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fmultiple%2Flifts.ma;h=7ae7099b6e79685bcf2ef1c995b6f294ff2bb369;hp=407a8d81019e5d3c034962d4dc8c391fe88de988;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hpb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma
index 407a8d810..7ae7099b6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma
@@ -12,16 +12,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/relocation/mr2_at.ma".
+include "ground_2/relocation/mr2_plus.ma".
 include "basic_2A/notation/relations/rliftstar_3.ma".
 include "basic_2A/substitution/lift.ma".
-include "basic_2A/multiple/mr2_plus.ma".
 
 (* GENERIC TERM RELOCATION **************************************************)
 
-inductive lifts: list2 nat nat → relation term ≝
+inductive lifts: mr2 → relation term ≝
 | 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)"
@@ -38,7 +39,7 @@ 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
@@ -46,7 +47,7 @@ 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-.
 
@@ -62,7 +63,7 @@ qed-.
 
 (* Basic_1: was: lift1_lref *)
 lemma lifts_inv_lref1: ∀T2,cs,i1. ⬆*[cs] #i1 ≡ T2 →
-                       ∃∃i2. @⦃i1, cs⦄ ≡ i2 & T2 = #i2.
+                       ∃∃i2. @❪i1, cs❫ ≘ i2 & T2 = #i2.
 #T2 #cs elim cs -cs
 [ #i1 #H <(lifts_inv_nil … H) -H /2 width=3 by at_nil, ex2_intro/
 | #l #m #cs #IH #i1 #H