have hexp_step := hneg htp
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
⊢ False
hneg : ∀ {e : FnExp} {τ : FnType}, e ∶ τ → Value e ∨ ∃ e', BadStep e e'
htp : app (app (fn 1) arg) arg ∶ argument
hexp_step : Value (app (app (fn 1) arg) arg) ∨ ∃ e', BadStep (app (app (fn 1) arg) arg) e'
⊢ False