(* Forward lemmas with parallel rst-computation for closures ****************)
(* Basic_2A1: uses: cprs_fpbs *)
-lemma cpms_fwd_fpbs (n) (h):
- ∀G,L,T1,T2. ❪G,L❫ ⊢ T1 ➡*[n,h] T2 → ❪G,L,T1❫ ≥[h] ❪G,L,T2❫.
-/3 width=2 by cpms_fwd_cpxs, cpxs_fpbs/ qed-.
+lemma cpms_fwd_fpbs (h) (n):
+ ∀G,L,T1,T2. ❪G,L❫ ⊢ T1 ➡*[h,n] T2 → ❪G,L,T1❫ ≥ ❪G,L,T2❫.
+/3 width=3 by cpms_fwd_cpxs, cpxs_fpbs/ qed-.