X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffle.ma;h=fdc03a5e2388869cc71ec99515f35d0ece4c1017;hp=02d3ecdb118d27724e6bbd33c2a3f7be4ede17d5;hb=b1868c5a258a6bf7fc983d63f3c417f00185e7b6;hpb=528f8ea107f689d07d060e1d31ba32bf65b4e6ba

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma
index 02d3ecdb1..fdc03a5e2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma
@@ -14,14 +14,14 @@
 
 include "ground_2/relocation/rtmap_id.ma".
 include "basic_2/notation/relations/subseteq_4.ma".
-include "basic_2/syntax/voids.ma".
+include "basic_2/syntax/lveq.ma".
 include "basic_2/static/frees.ma".
 
 (* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************)
 
 definition fle: bi_relation lenv term ≝ λL1,T1,L2,T2.
                 ∃∃n1,n2,f1,f2. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 &
-                               ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 & ⫱*[n1]f1 ⊆ ⫱*[n2]f2.
+                               L1 ≋ⓧ*[n1, n2] L2 & ⫱*[n1]f1 ⊆ ⫱*[n2]f2.
 
 interpretation "free variables inclusion (restricted closure)"
    'SubSetEq L1 T1 L2 T2 = (fle L1 T1 L2 T2).
@@ -29,12 +29,12 @@ interpretation "free variables inclusion (restricted closure)"
 (* Basic properties *********************************************************)
 
 lemma fle_sort: ∀L,s1,s2. ⦃L, ⋆s1⦄ ⊆ ⦃L, ⋆s2⦄.
-#L elim (voids_refl L)
+#L elim (lveq_refl L)
 /3 width=8 by frees_sort, sle_refl, ex4_4_intro/
 qed.
 
 lemma fle_gref: ∀L,l1,l2. ⦃L, §l1⦄ ⊆ ⦃L, §l2⦄.
-#L elim (voids_refl L)
+#L elim (lveq_refl L)
 /3 width=8 by frees_gref, sle_refl, ex4_4_intro/
 qed.