X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fdrops_ctc.ma;h=de5d1ce483209e7ce23d456f0f3a24546985206f;hp=cc485711c34f3d024c79b0eb9daf8c6c48d163bf;hb=222044da28742b24584549ba86b1805a87def070;hpb=54c4e854515cbcb1376881e9aedad006bf6545f2

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ctc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ctc.ma
index cc485711c..de5d1ce48 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ctc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ctc.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/lib/star.ma".
-include "basic_2/relocation/lreq_lreq.ma".
+include "basic_2/relocation/seq_seq.ma".
 
 (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
 
@@ -67,6 +67,6 @@ lemma co_dedropable_sn_CTC: ∀R. co_dedropable_sn R → co_dedropable_sn (CTC 
   /3 width=4 by inj, ex3_intro/
 | #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1
   #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -f1 -K
-  /3 width=6 by lreq_trans, step, ex3_intro/
+  /3 width=6 by seq_trans, step, ex3_intro/
 ]
 qed-.