X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffsle_fsle.ma;h=9468fe1c700b76b3c8ad47656d6629db6c5e2227;hp=deadd5cdc2908614e77668fbaa62d98328b70a02;hb=f7296f9cf2ee73465a374942c46b138f35c42ccb;hpb=e8971d3db8935436e6dddc27fe1ae168c7f3b315

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fsle_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fsle_fsle.ma
index deadd5cdc..9468fe1c7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/fsle_fsle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/fsle_fsle.ma
@@ -39,6 +39,15 @@ elim (lveq_inj_length … H2L) // -L2 #H1 #H2 destruct
 /2 width=3 by ex2_intro/
 qed-.
 
+lemma fsle_inv_frees_eq: ∀L1,L2. |L1| = |L2| →
+                         ∀T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ →
+                         ∀f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 →
+                         f1 ⊆ f2.
+#L1 #L2 #H1L #T1 #T2 #H2L #f1 #Hf1 #f2 #Hf2
+elim (fsle_frees_trans_eq … H2L … Hf2) // -L2 -T2
+/3 width=6 by frees_mono, sle_eq_repl_back1/
+qed-.
+
 (* Main properties **********************************************************)
 
 theorem fsle_trans_sn: ∀L1,L2,T1,T. ⦃L1, T1⦄ ⊆ ⦃L2, T⦄ →