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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_eq.ma
index b9574e479..9de1d40d7 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_eq.ma
@@ -21,7 +21,7 @@ include "delayed_updating/substitution/prelift_label_eq.ma".
 (* Constructions with path_eq ***********************************************)
 
 lemma lift_path_eq_repl (p):
-      stream_eq_repl … (λf1,f2. ↑[f1]p = ↑[f2]p).
+      stream_eq_repl … (λf1,f2. 🠡[f1]p = 🠡[f2]p).
 #p elim p -p //
 #l #p #IH #f1 #f2 #Hf
 <lift_path_rcons <lift_path_rcons