update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index 8d0cfc52dc46aca4d628c8e85381e1a8249543e6..d2a33afc211f1bb60396108e33a1362e6a6fb5b6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -28,8 +28,8 @@ include "ground/xoa/and_4.ma".
 definition ifr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃∃b,n.
            let r ≝ p●𝗔◗b●𝗟◗q in
-           â\88§â\88§ (â\8a\97b ϵ ð\9d\90\81 â\88§ ð\9d\9f\8e = â\9d\98bâ\9d\98) & â\86\91â\9d\98qâ\9d\98 = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
-              t1[â\8b\94râ\86\90â\86\91[ð\9d\90®â\9d¨â\9d\98bâ\97\8fð\9d\97\9fâ\97\97qâ\9d\98❩](t1⋔(p◖𝗦))] ⇔ t2
+           â\88§â\88§ (â\8a\97b ϵ ð\9d\90\81 â\88§ ð\9d\9f\8e = â\99­b) & â\86\91â\99­q = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
+              t1[â\8b\94râ\86\90â\86\91[ð\9d\90®â\9d¨â\99­(bâ\97\8fð\9d\97\9fâ\97\97q)❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation