-lemma rpx_inv_lpx_req: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 →
- ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h] L & L ≡[T] L2.
-/3 width=3 by rpx_fsge_comp, rex_inv_lex_req/ qed-.
+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_reqg_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 →
+ ∃∃L. ❨G,L1❩ ⊢ ⬈ L & L ≡[T] L2.
+/3 width=3 by rpx_fsge_comp, rex_fwd_lex_req/ qed-.