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 4f8c282b16a113c8aabb93a36cb986964075cb3f..746def17755b3f147022f07cb5773bb27121cbc5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -24,7 +24,7 @@ include "delayed_updating/notation/relations/black_rightarrow_f_4.ma".
 inductive ifr (p) (q) (t): predicate preterm ≝
 | ifr_beta (b):
   let r ≝ p●𝗔◗b●𝗟◗q in
-  r◖𝗱❨↑❘q❘❩ ϵ t → ⊓⊗b → ifr p q t (t[⋔r←↑[𝐮❨↑❘q❘❩]t⋔(p◖𝗦)])
+  r◖𝗱(↑❘q❘) ϵ t → ⊓(⊗b) → ifr p q t (t[⋔r←↑[𝐮❨↑❘q❘❩]t⋔(p◖𝗦)])
 .
 
 interpretation