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