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