-inductive lsred: rpointer → relation term ≝
-| lsred_beta : ∀A,D. lsred (◊) (@D.𝛌.A) ([⬐D]A)
-| lsred_abst : ∀p,A,C. lsred p A C → lsred p (𝛌.A) (𝛌.C)
-| lsred_appl_sn: ∀p,B,D,A. lsred p B D → lsred (true::p) (@B.A) (@D.A)
-| lsred_appl_dx: ∀p,B,A,C. lsred p A C → lsred (false::p) (@B.A) (@B.C)
+inductive lsred: ptr → relation term ≝
+| lsred_beta : ∀B,A. lsred (◊) (@B.𝛌.A) ([⬐B]A)
+| lsred_abst : ∀p,A1,A2. lsred p A1 A2 → lsred (rc::p) (𝛌.A1) (𝛌.A2)
+| lsred_appl_sn: ∀p,B1,B2,A. lsred p B1 B2 → lsred (sn::p) (@B1.A) (@B2.A)
+| lsred_appl_dx: ∀p,B,A1,A2. lsred p A1 A2 → lsred (dx::p) (@B.A1) (@B.A2)