update in ground

[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 f83cbdf88944adc56ef255f5d278866da4a57aca..d49e1608d2a6b162e33614431f83852b7e9f456c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma
@@ -20,7 +20,7 @@ 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
 .
@@ -30,12 +30,12 @@ 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 →