[Agda] Eta for Bool

[Swierstra, W.S. (Wouter)]

Dear all,

Suppose I have the following (silly) identity function:

   id : Bool -> Bool
   id True  = True
   id False = False

It's easy enough to show that this really is the identity function by 
proving:

  id-id : (b : Bool) -> id b ≡ b
  id-id True  = refl
  id-id False = refl

This is all easy enough -- but I've been writing a program where there 
are quite a few pattern matches of this form, often with the same (up to 
implicit arguments) right hand sides. Is there some idiom or eliminator 
that can reduce the amount of pattern matching required? I could write 
'id-id' using the usual eliminator for booleans, but I still need to 
pass in two copies of refl. What are my options for keeping the number 
of cases in check? Thanks in advance,

   Wouter