cases hf with
| fn =>
  apply Exists.intro (fn n)
  exact Step.appSucc
| appSucc => cases hval
case appSucc.h.inl
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hval : Value f
⊢ ∃ e', app f x ⇒ e'
no goals