induction hstep generalizing τ with
| @appArg f f' x h ih =>
  cases htp with
  | appZero hf hx =>
    apply HasType.appZero
    . exact ih hf
    . exact hx
  | @appSucc _ _ n hf hx =>
    apply HasType.appSucc
    . exact ih hf
    . exact hx
| @appZero x =>
  cases htp with
  | appZero => assumption
  | appSucc hf hx => cases hf
| @appSucc _ n =>
  cases htp with
  | appZero hf hx => cases hf
  | appSucc hf hx =>
    cases hf
    exact HasType.fn
e e' : FnExp
τ : FnType
htp : e ∶ τ
hstep : e ⇒ e'
⊢ e' ∶ τ
no goals