-lemma lpxs_pair_refl: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → ∀I,V. ⦃h, L1. ⓑ{I}V⦄ ⊢ ➡*[g] L2. ⓑ{I}V.
+lemma lpxs_strap2: ∀h,o,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡[h, o] L → ⦃G, L⦄ ⊢ ➡*[h, o] L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2.
+/2 width=3 by TC_strap/ qed.
+
+lemma lpxs_pair_refl: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡*[h, o] L2.ⓑ{I}V.