(* Main properties on the alternative definition ****************************)
-theorem lpxsa_lpxs: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡➡*[g] L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2.
+theorem lpxsa_lpxs: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡➡*[h, g] L2 → ⦃h, L1⦄ ⊢ ➡*[h, g] L2.
/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
(* Main inversion lemmas on the alternative definition **********************)
-theorem lpxs_inv_lpxsa: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → ⦃h, L1⦄ ⊢ ➡➡*[g] L2.
+theorem lpxs_inv_lpxsa: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L2 → ⦃h, L1⦄ ⊢ ➡➡*[h, g] L2.
/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpx_cpxs_trans/ qed-.
(* Alternative eliminators **************************************************)
lemma lpxs_ind_alt: ∀h,g. ∀R:relation lenv.
R (⋆) (⋆) → (
∀I,K1,K2,V1,V2.
- ⦃h, K1⦄ ⊢ ➡*[g] K2 → ⦃h, K1⦄ ⊢ V1 ➡*[g] V2 →
+ ⦃h, K1⦄ ⊢ ➡*[h, g] K2 → ⦃h, K1⦄ ⊢ V1 ➡*[h, g] V2 →
R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
) →
- ∀L1,L2. ⦃h, L1⦄ ⊢ ➡*[g] L2 → R L1 L2.
+ ∀L1,L2. ⦃h, L1⦄ ⊢ ➡*[h, g] L2 → R L1 L2.
/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-.