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 a8d9469ddaa6fe171c11ece64ebff473d74a3429..c555072f6558176f3d9d046ffb611e37fcf778c0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -26,7 +26,7 @@ lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
       t1 ➡𝐝𝐟[p,q] t2 → ↑[f]t1 ➡𝐟[⊗p,⊗q] ↑[f]t2.
 #f #p #q #t1 #t2 #H0t1
 * #b #n * #Hb #Hn  #Ht1 #Ht2
       t1 ➡𝐝𝐟[p,q] t2 → ↑[f]t1 ➡𝐟[⊗p,⊗q] ↑[f]t2.
 #f #p #q #t1 #t2 #H0t1
 * #b #n * #Hb #Hn  #Ht1 #Ht2

-@(ex1_2_intro … (⊗b) (❘⊗q❘)) @and4_intro
+@(ex1_2_intro â\80¦ (â\8a\97b) (â\86\91â\9d\98â\8a\97qâ\9d\98)) @and4_intro

 [ //
 | #g <lift_rmap_structure <depth_structure
   >tr_pushs_swap <tr_pap_pushs_le //
 [ //
 | #g <lift_rmap_structure <depth_structure
   >tr_pushs_swap <tr_pap_pushs_le //