interpretation "evaluation for context-sensitive extended parallel reduction (term)"
'PRedEval h g G L T1 T2 = (cpxe h g G L T1 T2).
-(* Basic_properties *********************************************************)
+(* Basic properties *********************************************************)
lemma csx_cpxe: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] 𝐍⦃T2⦄.
#h #g #G #L #T1 #H @(csx_ind … H) -T1