cases hexp_step with
| inl hval =>  cases hval
| inr hstep =>
  cases hstep with | intro e' he' =>
  cases he'
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
no goals