update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / lift_path_eq.ma

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 b9574e479e2a1115f0846aa5b09cad2d387b148e..9de1d40d77a5ebca0f5daf105aae5c657ee22236 100644 (file)
--- 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