-lemma rpx_inv_lpx_req (G):
- ∀L1,L2,T. ❪G,L1❫ ⊢ ⬈[T] L2 →
+lemma rpx_inv_req_lpx (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →
+ ∃∃L. L1 ≡[T] L & ❪G,L❫ ⊢ ⬈ L2.
+/4 width=13 by cpx_req_conf, rex_inv_req_lex, rex_conf1_next/ qed-.
+
+(* Forward lemmas with extended rt-transition for full local envs ***********)
+
+lemma rpx_fwd_lpx_req (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 →