update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
index be7f3b3d3d3825973ccb0af6aa5360a0cbb7b7a2..fd5f76b54ba8ff80a7d68ca8f2f9f186112bdba4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -33,7 +33,7 @@ include "delayed_updating/syntax/path_depth_reverse.ma".
 (* Main destructions with ifr ***********************************************)
 
 theorem dfr_des_ifr (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
-        t1 ➡𝐝𝐟[p,q] t2 → ▼[f]t1 ➡𝐟[⊗p,⊗q] ▼[f]t2.
+        t1 â\9e¡ð\9d\90\9dð\9d\90\9f[p,q] t2 â\86\92 â\96¼[f]t1 â\9e¡ð\9d\90¢ð\9d\90\9f[â\8a\97p,â\8a\97q] â\96¼[f]t2.
 #f #p #q #t1 #t2 #H0t1
 * #n * #H1n #Ht1 #Ht2
 @(ex_intro … (↑♭q)) @and3_intro