X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fllpx_sn_alt.ma;h=b2792cee246834f3ff7ca3a3f88e59b6ef31fcdc;hb=dffdece065d12d9961a6c3f1222f6d112030336f;hp=0916edb67f44c128874926132247e16bfa7705cc;hpb=87fbbf33fcc2ed91cc8b8a08e1c378ef49ac723d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt.ma
index 0916edb67..b2792cee2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt.ma
@@ -18,11 +18,11 @@ include "basic_2/substitution/llpx_sn_alt_rec.ma".
 (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
 
 (* alternative definition of llpx_sn (not recursive) *)
-definition llpx_sn_alt: relation4 bind2 lenv term term → relation4 ynat term lenv lenv ≝
+definition llpx_sn_alt: relation3 lenv term term → relation4 ynat term lenv lenv ≝
                         λR,d,T,L1,L2. |L1| = |L2| ∧
                         (∀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 ∧ R I1 K1 V1 V2
+                           I1 = I2 ∧ R K1 V1 V2
                         ).
 
 (* Main properties **********************************************************)