X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_lreq.ma;h=279ad0ca166f0d84f8c15d7df5361eede64b88ca;hb=e9da8e091898b6e67a2f270581bdc5cdbe80e9b0;hp=07e0d5e807fd33cd441c4147e29f200aff631b55;hpb=3a430d712f9d87185e9271b7b0c5188c5f311e4b;p=helm.git

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 07e0d5e80..279ad0ca1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_lreq.ma
@@ -19,22 +19,22 @@ include "basic_2/static/frees.ma".
 
 (* 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-.