apply HasType.appSucc
case appArg.appSucc
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ app f' x ∶ function n
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ f' ∶ function (Nat.succ n)

case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ x ∶ argument