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
case appArg
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
τ : FnType
htp : app f x ∶ τ
⊢ app f' x ∶ τ
no goals