cases hf
case appSucc.appSucc
e e' x✝ : FnExp
n n✝ : ℕ
hf : fn (Nat.succ n) ∶ function (Nat.succ n✝)
hx : x✝ ∶ argument
⊢ fn n ∶ function n✝
case appSucc.appSucc.fn
e e' x✝ : FnExp
n : ℕ
hx : x✝ ∶ argument
⊢ fn n ∶ function n