X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_drops.ma;h=f24e507850a21470569138388286bcde62428fc5;hb=02128ad2d07f4763e311a7f449d87aa022014c1f;hp=0e1ae0e21c115e56f95f077c4c707164e7da37c3;hpb=f6fd7c37170e17fa29ee835cdff3922ac11be398;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
index 0e1ae0e21..f24e50785 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
@@ -154,6 +154,12 @@ lemma frees_lifts: ∀b,f1,K,T. K ⊢ 𝐅*⦃T⦄ ≡ f1 →
 ]
 qed-.
 
+lemma frees_lifts_SO: ∀b,L,K. ⬇*[b, 𝐔❴1❵] L ≡ K → ∀T,U. ⬆*[1] T ≡ U →
+                      ∀f. K ⊢ 𝐅*⦃T⦄ ≡ f → L ⊢ 𝐅*⦃U⦄ ≡ ↑f.
+#b #L #K #HLK #T #U #HTU #f #Hf
+@(frees_lifts b … Hf … HTU) //  (**) (* auto fails *)
+qed.
+
 (* Forward lemmas with generic slicing for local environments ***************)
 
 lemma frees_fwd_coafter: ∀b,f2,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f2 →