X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops_ltc.ma;h=62ae1ecc6d00a1f082a90b8aaff2749788171db1;hp=3f999a5b2bfe75fe918a9fd48c4aad03c0bb9634;hb=222044da28742b24584549ba86b1805a87def070;hpb=5c186c72f508da0849058afeecc6877cd9ed6303

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ltc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ltc.ma
index 3f999a5b2..62ae1ecc6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ltc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ltc.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/lib/ltc.ma".
-include "basic_2/relocation/lreq_lreq.ma".
+include "basic_2/relocation/seq_seq.ma".
 
 (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
 
@@ -90,6 +90,6 @@ lemma co_dedropable_sn_ltc: ∀A,f. associative … f →
 | #n1 #n2 #K #K2 #_ #IH #HK2 #f2 #Hf
   elim (IH … Hf) -K1 -IH #L #H1L1 #HLK #H2L1
   elim (HR … HLK … HK2 … Hf) -f1 -K -HR
-  /3 width=6 by lreq_trans, ltc_dx, ex3_intro/
+  /3 width=6 by seq_trans, ltc_dx, ex3_intro/
 ]
 qed-.