update in ground, basic_2A and apps_2

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / functional / mf_cpr.ma

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.ma
index 70b98821cac444d14e1dc9e8c9ddc0b9f81d7532..26d43e20a133f87c805ca05810e4b408e34cbe73 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.ma
@@ -22,7 +22,7 @@ include "apps_2/functional/mf_exteq.ma".
 
 lemma mf_delta_drops (h) (G): ∀K,V1,V2. ❨G,K❩ ⊢ V1 ➡[h,0] V2 →
                               ∀T,L,i. ⇩[i] L ≘ K.ⓓV1 →
-                              â\88\80gv,lv. â\9d¨G,Lâ\9d© â\8a¢ â\97\8f[gv,â\87¡[iâ\86\90#i]lv]T â\9e¡[h,0] â\97\8f[gv,⇡[i←↑[↑i]V2]lv]T.
+                              â\88\80gv,lv. â\9d¨G,Lâ\9d© â\8a¢ â\96 [gv,â\87¡[iâ\86\90#i]lv]T â\9e¡[h,0] â\96 [gv,⇡[i←↑[↑i]V2]lv]T.
 #h #G #K #V1 #V2 #HV #T elim T -T * //
 [ #i #L #j #HKL #gv #lv
   >mf_lref >mf_lref