[Agda] again `with' vs `case'

[Nils Anders Danielsson]

On 2013-08-26 20:35, Sergei Meshveliani wrote:
> cong2-∈ {A = A} x (u ∷ xs) (v ∷ ys) (u=v ∷p =tail) x∈u-xs =

Note that the left-hand side above is rejected, even if you replace the
right-hand side with a question mark.

-- 
/NAD