- minor corrections

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_lreq.ma
index d0231ec6ac852ed4a95502dc8c80836eb6a6a36d..a1f7ab05ec15e057db640f2a2d284564d87fc760 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_lreq.ma
@@ -17,7 +17,7 @@ include "basic_2/relocation/frees.ma".
 
 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
 
-(* Properties on ranged equivalence for local environments ******************)
+(* 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