(* *)
(**************************************************************************)
+include "basic_2/notation/relations/predsnstar_4.ma".
include "basic_2/reduction/lpx.ma".
include "basic_2/computation/lprs.ma".
(* Basic properties *********************************************************)
-axiom lprs_lpxs: ∀h,g,L1,L2. L1 ⊢ ➡* L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2.
-(*
+lemma lprs_lpxs: ∀h,g,L1,L2. L1 ⊢ ➡* L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2.
/3 width=3/ qed.
-*)
+
lemma lpx_lpxs: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → ⦃h, L1⦄ ⊢ ➡*[g] L2.
/2 width=1/ qed.