induction htp with
| fn => exact Or.inl Value.fn
| arg => exact Or.inl Value.arg
| @appZero f x hf hx ihf ihx =>
  apply Or.inr
  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'      
| @appSucc f x n hf hx ihf ihx =>
  apply Or.inr
  cases ihf with
  | inl hval =>
    cases hf with
    | fn =>
      apply Exists.intro (fn n)
      exact Step.appSucc
    | appSucc => cases hval
  | inr hstep =>
    cases hstep with | intro f' hf' =>
    apply Exists.intro (app f' x)
    exact Step.appArg hf'
e : FnExp
τ : FnType
htp : e ∶ τ
⊢ Value e ∨ ∃ e', e ⇒ e'
no goals