update in ground and static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / frees_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma
index 7b4f04950b5d65b11741a5212f9432edeaf49191..69e0158e9539e102906928e9c9163d280dee365d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma
@@ -171,7 +171,7 @@ qed-.
 lemma frees_inv_lifts_SO:
       ∀b,f,L,U. L ⊢ 𝐅+❪U❫ ≘ f →
       ∀K. ⇩*[b,𝐔❨1❩] L ≘ K → ∀T. ⇧[1] T ≘ U →
-      K â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 ⫱f.
+      K â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 â«°f.
 #b #f #L #U #H #K #HLK #T #HTU elim(frees_inv_lifts_ex … H … HLK … HTU) -b -L -U
 #f1 #Hf #Hf1 elim (coafter_inv_nxx … Hf) -Hf
 /3 width=5 by frees_eq_repl_back, coafter_isid_inv_sn/
@@ -189,7 +189,7 @@ qed-.
 lemma frees_inv_drops_next:
       ∀f1,L1,T1. L1 ⊢ 𝐅+❪T1❫ ≘ f1 →
       ∀I2,L2,V2,i. ⇩[i] L1 ≘ L2.ⓑ[I2]V2 →
-      â\88\80g1. â\86\91g1 = ⫱*[i] f1 →
+      â\88\80g1. â\86\91g1 = â«°*[i] f1 →
       ∃∃g2. L2 ⊢ 𝐅+❪V2❫ ≘ g2 & g2 ⊆ g1.
 #f1 #L1 #T1 #H elim H -f1 -L1 -T1
 [ #f1 #L1 #s #Hf1 #I2 #L2 #V2 #j #_ #g1 #H1 -I2 -L1 -s