[Agda] refuting with rewrite

[Brandon Moore]

I see my example was insufficiently detailed.

In the real problem the equality involves a term rather than
a simple variable, and the term appears only in the
exposed with-clause of a partially reduced value.

It seems I must copy out the term and give it
a name in a with clause before it is possible
to pattern match on the equality.

This is exactly what rewrite was introduced to
avoid, so it's unfortunate it doesn't seem to work here.

module test where
data Bool : Set where true false : Bool
data ⊥ : Set where
data _≡_ (a : Bool) : Bool → Set where refl : a ≡ a

helper : Bool → Bool
helper true = true
helper false = false

fun : Bool → Bool
fun b with helper b
fun b | false = false
fun b | true = b

thm : (b : Bool) → (fun b ≡ true) → (helper b ≡ false) → ⊥
-- thm b () lem rewrite lem

thm b pf lem with helper b
thm b () refl | .false