-lemma scpds_strap1: ∀h,g,G,L,T1,T,T2,l.
- ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2.
-#h #g #G #L #T1 #T #T2 #l * /3 width=8 by cprs_strap1, ex4_2_intro/
+lemma scpds_strap1: ∀h,g,G,L,T1,T,T2,d.
+ ⦃G, L⦄ ⊢ T1 •*➡*[h, g, d] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, d] T2.
+#h #g #G #L #T1 #T #T2 #d * /3 width=8 by cprs_strap1, ex4_2_intro/