lemma lpx_append: ∀h,g,K1,K2. ⦃h, K1⦄ ⊢ ➡[g] K2 → ∀L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 →
⦃h, L1 @@ K1⦄ ⊢ ➡[g] L2 @@ K2.
/3 width=1 by lpx_sn_append, cpx_append/ qed.
lemma lpx_append: ∀h,g,K1,K2. ⦃h, K1⦄ ⊢ ➡[g] K2 → ∀L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 →
⦃h, L1 @@ K1⦄ ⊢ ➡[g] L2 @@ K2.
/3 width=1 by lpx_sn_append, cpx_append/ qed.