-lemma lprs_lpxs: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2.
-/3 width=3 by lpr_lpx, monotonic_TC/ qed.
+(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************)
+
+(* Forward lemmas with extended rt-computation for full local environments **)
+
+(* Basic_2A1: was: lprs_lpxs *)
+(* Note: original proof uses lpr_fwd_lpx and monotonic_TC *)
+lemma lprs_fwd_lpxs (h) (G):
+ ∀L1,L2. ❪G,L1❫ ⊢ ➡*[h,0] L2 → ❪G,L1❫ ⊢ ⬈* L2.
+/3 width=3 by cpms_fwd_cpxs, lex_co/ qed-.