update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / reduction / ifr_unwind.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
index 21e4ac27fac27dea7ae8c91a9ed629b509f3d66a..f05d86db3078678331cd649e9abe405996c383b1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
@@ -34,7 +34,7 @@ include "delayed_updating/syntax/path_depth_reverse.ma".
 
 lemma ifr_unwind_bi (f) (p) (q) (t1) (t2):
       t1 ϵ 𝐓 → t1⋔(p◖𝗦) ⧸≬ 𝐈 →
-      t1 â\9e¡ð\9d\90\9f[p,q] t2 â\86\92 â\96¼[f]t1 â\9e¡𝐟[⊗p,⊗q] ▼[f]t2.
+      t1 â\9e¡ð\9d\90¢ð\9d\90\9f[p,q] t2 â\86\92 â\96¼[f]t1 â\9e¡ð\9d\90¢𝐟[⊗p,⊗q] ▼[f]t2.
 #f #p #q #t1 #t2 #H1t1 #H2t1
 * #n * #H1n #Ht1 #Ht2
 @(ex_intro … (↑♭q)) @and3_intro