X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Flifts.ma;h=2721052555bdc6c63b8f7715e041fe6d670ebde3;hb=d6909ee6f43e0f29efbaf28b75b69723634c3af2;hp=67e93078e6bb8331fac52fbec14a9f9770181203;hpb=886d7c4b7a21b4ca8f148d42555a5d89e8222fc8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
index 67e93078e..272105255 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts.ma
@@ -19,7 +19,7 @@ include "basic_2/multiple/mr2_plus.ma".
 (* GENERIC TERM RELOCATION **************************************************)
 
 inductive lifts: list2 nat nat → relation term ≝
-| lifts_nil : ∀T. lifts (⟠) T T
+| lifts_nil : ∀T. lifts (◊) T T
 | lifts_cons: ∀T1,T,T2,des,d,e.
               ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2
 .
@@ -29,12 +29,12 @@ interpretation "generic relocation (term)"
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lifts_inv_nil_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → des = ⟠ → T1 = T2.
+fact lifts_inv_nil_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → des = ◊ → T1 = T2.
 #T1 #T2 #des * -T1 -T2 -des //
 #T1 #T #T2 #d #e #des #_ #_ #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,des. ⇧*[des] T1 ≡ T2 →