]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/multiple/frees.ma
- advances on free variables allow to reduce lleq_lpx_trans to llor_total :)
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / frees.ma
index 16c2af962919cd6d36def7dc5831d9b856db475b..f5e8f1c8872c4534d702548d07990e11620a88bd 100644 (file)
@@ -29,6 +29,9 @@ interpretation
    "context-sensitive free variables (term)"
    'FreeStar L i d U = (frees d L U i).
 
+definition frees_trans: predicate (relation3 lenv term term) ≝
+                        λR. ∀L,U1,U2,i. R L U1 U2 → L ⊢ i ϵ 𝐅*[0]⦃U2⦄ → L ⊢ i ϵ 𝐅*[0]⦃U1⦄.
+
 (* Basic inversion lemmas ***************************************************)
 
 lemma frees_inv: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →