[Agda] refuting with rewrite

[Brandon Moore]

Why doesn't this go through? It seems pointless to "with" on a trivial value
so the refutation can be written on the next line.

module test where
open import Relation.Binary.PropositionalEquality
open import Data.Bool
open import Data.Empty

data So : Bool → Set where oh : So true

fun : (b : Bool) → So b → b ≡ false → ⊥
fun b () eq rewrite eq