update in basic_2 + web page

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / lfxs_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
index 03772d98c9195bb7bfe04f588b14debc9ca36ae6..9e334565f386fc740e66a8f1bf9b6b19c905300e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
@@ -22,7 +22,7 @@ include "basic_2/static/lfxs.ma".
 definition dedropable_sn: predicate (relation3 lenv term term) ≝
                           λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 →
                           ∀K2,T. K1 ⪤*[R, T] K2 → ∀U. ⬆*[f] T ≡ U →
-                          â\88\83â\88\83L2. L1 ⪤*[R, U] L2 & â¬\87*[b, f] L2 â\89¡ K2 & L1 â\89¡[f] L2.
+                          â\88\83â\88\83L2. L1 ⪤*[R, U] L2 & â¬\87*[b, f] L2 â\89¡ K2 & L1 â\89\90[f] L2.
 
 definition dropable_sn: predicate (relation3 lenv term term) ≝
                         λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ →