I am extremely confused about this one.

• Given the following rule ("Type and Programming Languages", Benjamin Pierce, page 72):

(λx.t)v2 -> [x -> v2]t (* E-AppAbs*)

Later in the same book, at page 87, we have (I simplified):

let is_value (e : expr) =
  match e with
  | Abstr (_, _)->true
  | _ -> false

let rec step e =
  match e with
  | App(Abstr(x, t1), v2) when is_value v2 -> subst x v2 t1 (*E-AppAbs*)
  | App(e1, e2) when is_value e1 -> App (e1, step e2) (*E-App2*)
  | App(e1, e2) -> App(step e1, e2) (*E-App1*)
  | _ -> raise NoRuleApplies

Note that is_value v2 is a necessary precondition before calling subst. I hence, conclude that the term (λx.x)y Is not reducible, because y is not a an abstraction.

• However, I keep seeing this:

(this is a screenshot from a Chicago university pdf, page 4)

Similarly, here, we can see that the accepted answers does:

(λx.xy)z   ->*   zy

This comes as contradiction to me, because, again, z above is not an abstraction.

Question: I don't understand what I am missing in definition, and why everyone keeps reducing stuff?