cases he'
case inr.intro
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
e' : FnExp
he' : BadStep (app (app (fn 1) arg) arg) e'
⊢ False
no goals