(**************************************************************************)
include "static_2/static/rex_lex.ma".
(**************************************************************************)
include "static_2/static/rex_lex.ma".
include "basic_2/rt_transition/lpx.ma".
(* EXTENDED PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS **********)
include "basic_2/rt_transition/lpx.ma".
(* EXTENDED PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS **********)
lemma rpx_inv_req_lpx (G) (T):
∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →
∃∃L. L1 ≡[T] L & ❪G,L❫ ⊢ ⬈ L2.
lemma rpx_inv_req_lpx (G) (T):
∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →
∃∃L. L1 ≡[T] L & ❪G,L❫ ⊢ ⬈ L2.