X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Freduction%2Fdfr_ifr.ma;h=c555072f6558176f3d9d046ffb611e37fcf778c0;hb=80ecd5486c6013f6c297173f41432fd1d93814ef;hp=a8d9469ddaa6fe171c11ece64ebff473d74a3429;hpb=8d8863982ca95225551e9659ed431db046c34e81;p=helm.git

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 a8d9469dd..c555072f6 100644
--- 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
-@(ex1_2_intro … (⊗b) (❘⊗q❘)) @and4_intro
+@(ex1_2_intro … (⊗b) (↑❘⊗q❘)) @and4_intro
 [ //
 | #g <lift_rmap_structure <depth_structure
   >tr_pushs_swap <tr_pap_pushs_le //