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

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
index aa9bc1b276f3698351972ebdbcd6eb60db636e27..a05a51d268e800b2b9d977ea04e20782fff73047 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
@@ -20,7 +20,7 @@ include "basic_2/substitution/lleq.ma".
 (* Alternative definition (not recursive) ***********************************)
 
 theorem lleq_intro_alt: ∀L1,L2,T,d. |L1| = |L2| →
-                        (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) →
+                        (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ →
                            ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
                            I1 = I2 ∧ V1 = V2
                         ) → L1 ≡[T, d] L2.
@@ -31,7 +31,7 @@ qed.
 
 theorem lleq_inv_alt: ∀L1,L2,T,d. L1 ≡[T, d] L2 →
                       |L1| = |L2| ∧
-                      ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) →
+                      ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ →
                       ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
                       I1 = I2 ∧ V1 = V2.
 #L1 #L2 #T #d #H elim (llpx_sn_llpx_sn_alt … H) -H