X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Frsx_drops.ma;h=6894a72aa2709afb8102f74fac063489c3a92453;hb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;hp=b8d78ca674dbb34472a340c1584c82e840bd0330;hpb=3c7b4071a9ac096b02334c1d47468776b948e2de;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
index b8d78ca67..6894a72aa 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rsx_drops.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/static/reqx_drops.ma".
+include "static_2/static/reqg_drops.ma".
 include "basic_2/rt_transition/lpx_drops.ma".
 include "basic_2/rt_computation/rsx_length.ma".
 include "basic_2/rt_computation/rsx_fqup.ma".
@@ -28,7 +28,7 @@ lemma rsx_lifts (G):
 #G #K #T #H @(rsx_ind … H) -K
 #K1 #_ #IH #b #f #L1 #HLK1 #Hf #U #HTU @rsx_intro
 #L2 #HL12 #HnL12 elim (lpx_drops_conf … HLK1 … HL12)
-/5 width=9 by reqx_lifts_bi, lpx_fwd_length/
+/5 width=9 by reqg_lifts_bi, lpx_fwd_length/
 qed-.
 
 (* Inversion lemmas on relocation *******************************************)
@@ -39,7 +39,7 @@ lemma rsx_inv_lifts (G):
 #G #L #U #H @(rsx_ind … H) -L
 #L1 #_ #IH #b #f #K1 #HLK1 #Hf #T #HTU @rsx_intro
 #K2 #HK12 #HnK12 elim (drops_lpx_trans … HLK1 … HK12) -HK12
-/4 width=10 by reqx_inv_lifts_bi/
+/4 width=10 by reqg_inv_lifts_bi/
 qed-.
 
 (* Advanced properties ******************************************************)