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 07e0d5e807fd33cd441c4147e29f200aff631b55..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
@@ -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-.