X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Ffsubst_lift.ma;h=ad0de7230e87c803d0aade06d7b13f53738f9ab3;hp=383bc24f9b28519f680b4ac530a2de2fe5af8717;hb=7008128d354c6e998a87bc2febe9f86ea714869c;hpb=d06053844638d88936d711b66fddbcca2a9add1c

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
index 383bc24f9..ad0de7230 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
@@ -20,7 +20,7 @@ include "delayed_updating/substitution/lift_prototerm_eq.ma".
 (* Constructions with lift for preterm **************************************)
 
 lemma lift_term_fsubst_sn (f) (t) (u) (p):
-      (â[f]t)[â(â[f]p)ââ[â[p]f]u] â â[f](t[âpâu]).
+      (ð ¡[f]t)[â(ð ¡[f]p)âð ¡[ð ¢[f]p]u] â ð ¡[f](t[âpâu]).
 #f #t #u #p #ql * *
 [ #rl * #r #Hr #H1 #H2 destruct
   >lift_path_append
@@ -32,7 +32,7 @@ lemma lift_term_fsubst_sn (f) (t) (u) (p):
 qed-.
 
 lemma lift_term_fsubst_dx (f) (t) (u) (p):
-      â[f](t[âpâu]) â (â[f]t)[â(â[f]p)ââ[â[p]f]u].
+      ð ¡[f](t[âpâu]) â (ð ¡[f]t)[â(ð ¡[f]p)âð ¡[ð ¢[f]p]u].
 #f #t #u #p #ql * #q * *
 [ #r #Hu #H1 #H2 destruct
   @or_introl @ex2_intro
@@ -47,5 +47,5 @@ lemma lift_term_fsubst_dx (f) (t) (u) (p):
 qed-.
 
 lemma lift_term_fsubst (f) (t) (u) (p):
-      (â[f]t)[â(â[f]p)ââ[â[p]f]u] â â[f](t[âpâu]).
+      (ð ¡[f]t)[â(ð ¡[f]p)âð ¡[ð ¢[f]p]u] â ð ¡[f](t[âpâu]).
 /3 width=1 by lift_term_fsubst_sn, conj, lift_term_fsubst_dx/ qed.