cases hval with
| @fn n =>
  cases hf
  apply Exists.intro x
  apply Step.appZero
| arg => cases hf
case appZero.h.inl
e : FnExp
τ : FnType
f x : FnExp
hf : f ∶ function 0
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
hval : Value f
⊢ ∃ e', app f x ⇒ e'
no goals