cases hf
case appZero.h.inl.fn
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
n : ℕ
hf : fn n ∶ function 0
⊢ ∃ e', app (fn n) x ⇒ e'
case appZero.h.inl.fn.fn
e : FnExp
τ : FnType
x : FnExp
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
⊢ ∃ e', app (fn 0) x ⇒ e'