(* *)
(**************************************************************************)
-include "basic_2/static/lfdeq_fqup.ma".
+include "static_2/static/rdeq_fqup.ma".
include "basic_2/rt_computation/rdsx.ma".
(* STRONGLY NORMALIZING REFERRED LOCAL ENV.S FOR UNBOUND RT-TRANSITION ******)
@(rdsx_ind … H) -L #L1 #_ #IH
@rdsx_intro #Y #H #HT
elim (lpx_inv_unit_sn … H) -H #L2 #HL12 #H destruct
-/4 width=4 by lfdeq_fwd_bind_dx_void/
+/4 width=4 by rdeq_fwd_bind_dx_void/
qed-.
(* Advanced inversion lemmas ************************************************)