/3 width=5 by jsx_fwd_lsubr, csx_lsubr_conf/ qed-.
(* Properties with strongly rt-normalizing referred local environments ******)
(* Note: Try by induction on the 2nd premise by generalizing V with f *)
lemma rsx_jsx_trans (h) (G):
/3 width=5 by jsx_fwd_lsubr, csx_lsubr_conf/ qed-.
(* Properties with strongly rt-normalizing referred local environments ******)
(* Note: Try by induction on the 2nd premise by generalizing V with f *)
lemma rsx_jsx_trans (h) (G):