X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffsle.ma;h=9f4f9cf3b07c8e73d35ac0d57c83dd023fd34e4a;hp=e0ef144b5a82dead9489223ad815ed82757b81dc;hb=222044da28742b24584549ba86b1805a87def070;hpb=990f97071a9939d47be16b36f6045d3b23f218e0

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fsle.ma
index e0ef144b5..9f4f9cf3b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/fsle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/fsle.ma
@@ -20,7 +20,7 @@ include "basic_2/static/frees.ma".
 (* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************)
 
 definition fsle: bi_relation lenv term ≝ λL1,T1,L2,T2.
-                 ∃∃n1,n2,f1,f2. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 &
+                 ∃∃n1,n2,f1,f2. L1 ⊢ 𝐅*⦃T1⦄ ≘ f1 & L2 ⊢ 𝐅*⦃T2⦄ ≘ f2 &
                                 L1 ≋ⓧ*[n1, n2] L2 & ⫱*[n1]f1 ⊆ ⫱*[n2]f2.
 
 interpretation "free variables inclusion (restricted closure)"