X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts_vector.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts_vector.ma;h=23d54010d95aceae6fe4f0261f4e70d59f920c33;hb=12dc655b7f5321b33b93a310d53e23e60e090caa;hp=d0cd506bc8f00549b6cc2aa7cb0177cc0876b149;hpb=dd41efaab7f147d5673cc30a27d36375f9b52c9d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma
index d0cd506bc..23d54010d 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma
@@ -19,7 +19,7 @@ include "static_2/relocation/lifts.ma".
 
 (* Basic_2A1: includes: liftv_nil liftv_cons *)
 inductive liftsv (f): relation … ≝
-| liftsv_nil : liftsv f (Ⓔ) (Ⓔ)
+| liftsv_nil : liftsv f (ⓔ) (ⓔ)
 | liftsv_cons: ∀T1s,T2s,T1,T2.
                ⇧*[f] T1 ≘ T2 → liftsv f T1s T2s →
                liftsv f (T1 ⨮ T1s) (T2 ⨮ T2s)
@@ -34,14 +34,14 @@ interpretation "uniform relocation (term vector)"
 (* Basic inversion lemmas ***************************************************)
 
 fact liftsv_inv_nil1_aux (f):
-     ∀X,Y. ⇧*[f] X ≘ Y → X = Ⓔ → Y = Ⓔ.
+     ∀X,Y. ⇧*[f] X ≘ Y → X = ⓔ → Y = ⓔ.
 #f #X #Y * -X -Y //
 #T1s #T2s #T1 #T2 #_ #_ #H destruct
 qed-.
 
 (* Basic_2A1: includes: liftv_inv_nil1 *)
 lemma liftsv_inv_nil1 (f):
-      ∀Y. ⇧*[f] Ⓔ ≘ Y → Y = Ⓔ.
+      ∀Y. ⇧*[f] ⓔ ≘ Y → Y = ⓔ.
 /2 width=5 by liftsv_inv_nil1_aux/ qed-.
 
 fact liftsv_inv_cons1_aux (f):
@@ -60,13 +60,13 @@ lemma liftsv_inv_cons1 (f):
 /2 width=3 by liftsv_inv_cons1_aux/ qed-.
 
 fact liftsv_inv_nil2_aux (f):
-     ∀X,Y. ⇧*[f] X ≘ Y → Y = Ⓔ → X = Ⓔ.
+     ∀X,Y. ⇧*[f] X ≘ Y → Y = ⓔ → X = ⓔ.
 #f #X #Y * -X -Y //
 #T1s #T2s #T1 #T2 #_ #_ #H destruct
 qed-.
 
 lemma liftsv_inv_nil2 (f):
-      ∀X. ⇧*[f] X ≘ Ⓔ → X = Ⓔ.
+      ∀X. ⇧*[f] X ≘ ⓔ → X = ⓔ.
 /2 width=5 by liftsv_inv_nil2_aux/ qed-.
 
 fact liftsv_inv_cons2_aux (f):