[Agda] `case' vs `with'

[Serge D. Mechveliani]

Agda has taken much of syntax from the Haskell language,
and I like this.
But why	does not it take the `case' construct?
For example, each of

  toFin r = case  lessEq r g  of
                              yes p -> natToFin g r p
                              _     -> natToFin g 0 (z<=n)
and
  toFin r = case  lessEq r g
            of
            yes p -> natToFin g r p
            _     -> natToFin g 0 (z<=n)

is easier to read than

  toFin r  with  lessEq r g
  ... | yes p = natToFin g r p
  ... | _     = natToFin g 0 (z<=n)

(`of' instead of  `... |').
`->' can be replaced say with `|->',  if it is needed to stress the 
difference to forming a function type.  

Regards,

------
Sergei