update in ground

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / lifts_vector.ma

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 d0cd506bc8f00549b6cc2aa7cb0177cc0876b149..23d54010d95aceae6fe4f0261f4e70d59f920c33 100644 (file)
--- 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 (â\92º) (â\92º)
+| liftsv_nil : liftsv f (â\93\94) (â\93\94)
 | 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):
-     â\88\80X,Y. â\87§*[f] X â\89\98 Y â\86\92 X = â\92º â\86\92 Y = â\92º.
+     â\88\80X,Y. â\87§*[f] X â\89\98 Y â\86\92 X = â\93\94 â\86\92 Y = â\93\94.
 #f #X #Y * -X -Y //
 #T1s #T2s #T1 #T2 #_ #_ #H destruct
 qed-.
 
 (* Basic_2A1: includes: liftv_inv_nil1 *)
 lemma liftsv_inv_nil1 (f):
-      â\88\80Y. â\87§*[f] â\92º â\89\98 Y â\86\92 Y = â\92º.
+      â\88\80Y. â\87§*[f] â\93\94 â\89\98 Y â\86\92 Y = â\93\94.
 /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):
-     â\88\80X,Y. â\87§*[f] X â\89\98 Y â\86\92 Y = â\92º â\86\92 X = â\92º.
+     â\88\80X,Y. â\87§*[f] X â\89\98 Y â\86\92 Y = â\93\94 â\86\92 X = â\93\94.
 #f #X #Y * -X -Y //
 #T1s #T2s #T1 #T2 #_ #_ #H destruct
 qed-.
 
 lemma liftsv_inv_nil2 (f):
-      â\88\80X. â\87§*[f] X â\89\98 â\92º â\86\92 X = â\92º.
+      â\88\80X. â\87§*[f] X â\89\98 â\93\94 â\86\92 X = â\93\94.
 /2 width=5 by liftsv_inv_nil2_aux/ qed-.
 
 fact liftsv_inv_cons2_aux (f):