renaming in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / drops_ltc.ma

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 3f999a5b2bfe75fe918a9fd48c4aad03c0bb9634..62ae1ecc6d00a1f082a90b8aaff2749788171db1 100644 (file)
--- 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-.