X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffrees_drops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffrees_drops.ma;h=69e0158e9539e102906928e9c9163d280dee365d;hb=dc605ae41c39773f55381f241b1ed3db4acf5edd;hp=7b4f04950b5d65b11741a5212f9432edeaf49191;hpb=caf822cbe34e204e6d1b72e272373b561c1a565a;p=helm.git

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 7b4f04950..69e0158e9 100644
--- 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 ⊢ 𝐅+❪T❫ ≘ ⫱f.
+      K ⊢ 𝐅+❪T❫ ≘ ⫰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 →
-      ∀g1. ↑g1 = ⫱*[i] f1 →
+      ∀g1. ↑g1 = ⫰*[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