definition cix: ∀h. sd h → relation3 genv lenv term ≝
λh,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⊥.
definition cix: ∀h. sd h → relation3 genv lenv term ≝
λh,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⊥.
-interpretation "context-sensitive extended irreducibility (term)"
- 'NotReducible h g G L T = (cix h g G L T).
+interpretation "irreducibility for context-sensitive extended reduction (term)"
+ 'PRedNotReducible h g G L T = (cix h g G L T).