-lemma lpr_cprs_yprs: ∀h,g,L1,L2,T1,T2. L1 ⊢ ➡ L2 → L2 ⊢ T1 ➡* T2 →
- h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
-/3 width=4 by yprs_strap2, ypr_lpr, cprs_yprs/
-qed.
+lemma cpr_lpr_yprs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 →
+ ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄.
+/4 width=5 by yprs_strap1, ypr_lpr, ypr_cpr/ qed.
+
+lemma ssta_yprs: ∀h,g,G,L,T,U,l.
+ ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U →
+ ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄.
+/3 width=2 by ypr_yprs, ypr_ssta/ qed.