apply Exists.intro (app f' x)
case appSucc.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ ∃ e', app f x ⇒ e'
case appSucc.h.inr.intro
e : FnExp
τ : FnType
f x : FnExp
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
ihx : Value x ∨ ∃ e', x ⇒ e'
f' : FnExp
hf' : f ⇒ f'
⊢ app f x ⇒ app f' x