(* STRONGLY NORMALIZING REFERRED LOCAL ENVS FOR EXTENDED RT-TRANSITION ******)
definition rsx (G) (T): predicate lenv ≝
(* STRONGLY NORMALIZING REFERRED LOCAL ENVS FOR EXTENDED RT-TRANSITION ******)
definition rsx (G) (T): predicate lenv ≝
∀I,K,V. L = K.ⓑ[I]V → G ⊢ ⬈*𝐒[V] K.
#G #L #H
@(rsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct
∀I,K,V. L = K.ⓑ[I]V → G ⊢ ⬈*𝐒[V] K.
#G #L #H
@(rsx_ind … H) -L #L1 #_ #IH #I #K1 #V #H destruct