-lemma cprs_scpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ➡* T2 →
- ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2.
-/2 width=6 by lstar_O, ex4_2_intro/ qed.
-
-lemma scpds_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*➡*[h, g, 0] T.
-/2 width=2 by cprs_scpds/ qed.
-