X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffsle_fsle.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffsle_fsle.ma;h=e97d5e4c1c0c83279caf2d064b302e19e2474ab5;hb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;hp=588182317cdf7db2a2614bd0b2d76aac30b45061;hpb=adb9ba187619cea977d1d22971eba27eb437cd6a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/fsle_fsle.ma b/matita/matita/contribs/lambdadelta/static_2/static/fsle_fsle.ma
index 588182317..e97d5e4c1 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/fsle_fsle.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/fsle_fsle.ma
@@ -19,7 +19,7 @@ include "static_2/static/fsle_fqup.ma".
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma fsle_frees_trans: 
+lemma fsle_frees_trans:
       ∀L1,L2,T1,T2. ⦃L1,T1⦄ ⊆ ⦃L2,T2⦄ →
       ∀f2. L2 ⊢ 𝐅+⦃T2⦄ ≘ f2 →
       ∃∃n1,n2,f1. L1 ⊢ 𝐅+⦃T1⦄ ≘ f1 & L1 ≋ⓧ*[n1,n2] L2 & ⫱*[n1]f1 ⊆ ⫱*[n2]f2.