-(* Basic_2A1: was just: lpxs_strap2 *)
-lemma lfpxs_strap2: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
-/2 width=3 by TC_strap/ qed.
-(*
-(* Basic_2A1: was just: lpxs_pair_refl *)
-lemma lfpxs_pair_refl: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈*[h, T] L2.ⓑ{I}V.
-/2 width=1 by TC_lpx_sn_pair_refl/ qed.
+lemma lfpxs_step_sn: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
+/2 width=3 by tc_lfxs_step_sn/ qed.