- advances on hereditarily free variables: now "frees" is primitive

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / llor.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma
index 2c1b48ad90699c88e2977c116b474f51646a22ca..94dfeeb256e2561f16589a64add1c4efe107690d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lazyor_4.ma".
-include "basic_2/substitution/cofrees.ma".
+include "basic_2/substitution/frees.ma".
 
 (* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
 
@@ -21,8 +21,8 @@ definition llor: relation4 term lenv lenv lenv ≝ λT,L2,L1,L.
                  ∧∧ |L1| ≤ |L2| & |L1| = |L|
                   & (∀I1,I2,I,K1,K2,K,V1,V2,V,i.
                        ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → ⇩[i] L ≡ K.ⓑ{I}V →
-                       (∧∧ L1 ⊢ i ~ϵ 𝐅*[yinj 0]⦃T⦄ & I1 = I & V1 = V) ∨
-                       (∧∧ (L1 ⊢ i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) & I1 = I & V2 = V)
+                       (∧∧ (L1 ⊢ i ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) & I1 = I & V1 = V) ∨
+                       (∧∧ L1 ⊢ i ϵ 𝐅*[yinj 0]⦃T⦄  & I1 = I & V2 = V)
                     ).
 
 interpretation
@@ -36,5 +36,3 @@ lemma llor_atom: ∀T,L2. ⋆ ⩖[T] L2 ≡ ⋆.
 #I1 #I2 #I #K1 #K2 #K #V1 #V2 #V #i #HLK1
 elim (ldrop_inv_atom1 … HLK1) -HLK1 #H destruct
 qed.
-
-axiom llor_total: ∀L1,L2,T. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L.