exfalso/exact taking argument

Stream: general

[Eric Rodriguez]

I always thought it'd be nice to be able to, for h : false, exact h, or at least exfalso h to close the goal. sometimes exact (...).elim can get unwieldy. am I missing a tactic?

[Eric Rodriguez]

oh, this is cases, d'ah