X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fllpx_sn_tc.ma;h=13fc14e82d62a11e7d016eb239edd49f04d9a5f3;hb=2c8220e5e0c09486355aa79d5cd8a7716c444aca;hp=866f8fdd22d9a54efe196fede02ef8039d8ef641;hpb=f282b35b958c9602fb1f47e5677b5805a046ac76;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_tc.ma
index 866f8fdd2..13fc14e82 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_tc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_tc.ma
@@ -12,14 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/llpx_sn_ldrop.ma".
+include "basic_2/multiple/llpx_sn_drop.ma".
 
 (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
 
 (* Properties about transitive closure **************************************)
 
-lemma llpx_sn_TC_pair_dx: ∀R. (∀I,L. reflexive … (R I L)) →
-                          ∀I,L,V1,V2,T. LTC … (R I) L V1 V2 →
+lemma llpx_sn_TC_pair_dx: ∀R. (∀L. reflexive … (R L)) →
+                          ∀I,L,V1,V2,T. LTC … R L V1 V2 →
                           LTC … (llpx_sn R 0) T (L.ⓑ{I}V1) (L.ⓑ{I}V2).
 #R #HR #I #L #V1 #V2 #T #H @(TC_star_ind … V2 H) -V2
 /4 width=9 by llpx_sn_bind_repl_O, llpx_sn_refl, step, inj/