[Agda] refuting with rewrite

[Nils Anders Danielsson]

On 2011-03-09 17:12, Brandon Moore wrote:
> 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

The rewrite construct introduces a helper function (via with), so you
cannot take advantage of a rewrite in the original patterns, as in

   thm b () lem rewrite lem.

However, the following code works:

   thm b pf lem rewrite lem with pf
   ... | ()

-- 
/NAD