some renaming and reordering of variables

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / frees_lreq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma
index a1f7ab05ec15e057db640f2a2d284564d87fc760..279ad0ca166f0d84f8c15d7df5361eede64b88ca 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma
@@ -13,28 +13,28 @@
 (**************************************************************************)
 
 include "basic_2/relocation/lreq.ma".
-include "basic_2/relocation/frees.ma".
+include "basic_2/static/frees.ma".
 
 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
 
 (* Properties with ranged equivalence for local environments ****************)
 
-lemma frees_lreq_conf: ∀L1,T,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L1 ≡[f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
-#L1 #T #f #H elim H -L1 -T -f
-[ #I #f #Hf #X #H lapply (lreq_inv_atom1 … H) -H
+lemma frees_lreq_conf: ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L1 ≡[f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
+#f #L1 #T #H elim H -f -L1 -T
+[ #f #I #Hf #X #H lapply (lreq_inv_atom1 … H) -H
   #H destruct /2 width=1 by frees_atom/
-| #I #L1 #V1 #s #f #_ #IH #X #H elim (lreq_inv_push1 … H) -H
+| #f #I #L1 #V1 #s #_ #IH #X #H elim (lreq_inv_push1 … H) -H
   /3 width=1 by frees_sort/
-| #I #L1 #V1 #f #_ #IH #X #H elim (lreq_inv_next1 … H) -H
+| #f #I #L1 #V1 #_ #IH #X #H elim (lreq_inv_next1 … H) -H
   /3 width=1 by frees_zero/
-| #I #L1 #V1 #i #f #_ #IH #X #H elim (lreq_inv_push1 … H) -H
+| #f #I #L1 #V1 #i #_ #IH #X #H elim (lreq_inv_push1 … H) -H
   /3 width=1 by frees_lref/
-| #I #L1 #V1 #l #f #_ #IH #X #H elim (lreq_inv_push1 … H) -H
+| #f #I #L1 #V1 #l #_ #IH #X #H elim (lreq_inv_push1 … H) -H
   /3 width=1 by frees_gref/
 | /6 width=5 by frees_bind, lreq_inv_tl, sle_lreq_trans, sor_inv_sle_dx, sor_inv_sle_sn/
 | /5 width=5 by frees_flat, sle_lreq_trans, sor_inv_sle_dx, sor_inv_sle_sn/
 ]
 qed-.
 
-lemma lreq_frees_trans: ∀L1,T,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L2 ≡[f] L1 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
+lemma lreq_frees_trans: ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L2 ≡[f] L1 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
 /3 width=3 by frees_lreq_conf, lreq_sym/ qed-.