(* *)
(**************************************************************************)
-include "static_2/static/reqx_fqup.ma".
+include "static_2/static/reqg_fqup.ma".
include "basic_2/rt_computation/rsx.ma".
(* STRONGLY NORMALIZING REFERRED LOCAL ENVS FOR EXTENDED RT-TRANSITION ******)
#G #T
@rsx_intro #Y #H #HnT
lapply (lpx_inv_atom_sn … H) -H #H destruct
-elim HnT -HnT //
+elim HnT -HnT /2 width=1 by rex_refl/
qed.
(* Advanced forward lemmas **************************************************)
@(rsx_ind … H) -L #L1 #_ #IH
@rsx_intro #Y #H #HT
elim (lpx_inv_unit_sn … H) -H #L2 #HL12 #H destruct
-/4 width=4 by reqx_fwd_bind_dx_void/
+/4 width=4 by reqg_fwd_bind_dx_void/
qed-.
(* Advanced inversion lemmas ************************************************)