X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffle_drops.ma;h=c64e197ef122fef84eff1c9b93795e5fbd5e263c;hp=39bf29385c2ffb83736ff0b51878f564f2b8424c;hb=93db728b3f690d2c683f64833353da685a6f1b65;hpb=9323611e3819c1382b872a7ada00264991f36217

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_drops.ma
index 39bf29385..c64e197ef 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/fle_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_drops.ma
@@ -30,6 +30,16 @@ lapply (frees_lifts_SO (Ⓣ) (L1.ⓧ) … HTU1 … Hf)
 @(ex4_4_intro … Hf Hg) /2 width=4 by lveq_void_sn/ (**) (* explict constructor *)
 qed-.
 
+lemma fle_lifts_SO: ∀K1,K2. |K1| = |K2| → ∀T1,T2. ⦃K1, T1⦄ ⊆ ⦃K2, T2⦄ →
+                    ∀U1,U2. ⬆*[1] T1 ≡ U1 → ⬆*[1] T2 ≡ U2 →
+                    ∀I1,I2.  ⦃K1.ⓘ{I1}, U1⦄ ⊆ ⦃K2.ⓘ{I2}, U2⦄.
+#K1 #K2 #HK #T1 #T2
+* #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12
+#U1 #U2 #HTU1 #HTU2 #I1 #I2
+elim (lveq_inj_length … HK12) // -HK #H1 #H2 destruct
+/5 width=12 by frees_lifts_SO, drops_refl, drops_drop, lveq_bind, sle_push, ex4_4_intro/
+qed.
+
 (* Advanced inversion lemmas ************************************************)
 
 lemma fle_inv_lifts_sn: ∀T1,U1. ⬆*[1] T1 ≡ U1 →