X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Frdsx_drops.ma;h=6f0cc4da05bfa08937ec883b3e027a44f0a64f78;hp=db1bd514444bfa17aeee340a409a556dfee3753d;hb=222044da28742b24584549ba86b1805a87def070;hpb=5c186c72f508da0849058afeecc6877cd9ed6303

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_drops.ma
index db1bd5144..6f0cc4da0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_drops.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/static/lfdeq_drops.ma".
+include "basic_2/static/rdeq_drops.ma".
 include "basic_2/rt_transition/lpx_drops.ma".
 include "basic_2/rt_computation/rdsx_length.ma".
 include "basic_2/rt_computation/rdsx_fqup.ma".
@@ -27,7 +27,7 @@ lemma rdsx_lifts (h) (o) (G): d_liftable1_isuni … (λL,T. G ⊢ ⬈*[h, o, T]
 #h #o #G #K #T #H @(rdsx_ind … H) -K
 #K1 #_ #IH #b #f #L1 #HLK1 #Hf #U #HTU @rdsx_intro
 #L2 #HL12 #HnL12 elim (lpx_drops_conf … HLK1 … HL12) 
-/5 width=9 by lfdeq_lifts_bi, lpx_fwd_length/
+/5 width=9 by rdeq_lifts_bi, lpx_fwd_length/
 qed-.
 
 (* Inversion lemmas on relocation *******************************************)
@@ -37,7 +37,7 @@ lemma rdsx_inv_lifts (h) (o) (G): d_deliftable1_isuni … (λL,T. G ⊢ ⬈*[h,
 #h #o #G #L #U #H @(rdsx_ind … H) -L
 #L1 #_ #IH #b #f #K1 #HLK1 #Hf #T #HTU @rdsx_intro
 #K2 #HK12 #HnK12 elim (drops_lpx_trans … HLK1 … HK12) -HK12
-/4 width=10 by lfdeq_inv_lifts_bi/
+/4 width=10 by rdeq_inv_lifts_bi/
 qed-.
 
 (* Advanced properties ******************************************************)