[Agda] missed wildcard pattern

[Sergei Meshveliani]

Dear Agda developers,
I have the following question about the Agda language.
Consider the program

------------------------------------------------------------------------
open import Relation.Binary  using (Decidable)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open import Data.Empty using (⊥-elim)
open import Data.Nat   using (ℕ)

data Expr : Set where :0   : Expr
                      gen  : ℕ → Expr
                      _+_  : Expr → Expr → Expr
	           -- _*_  : Expr → Expr → Expr    -- reserve

f : Expr → Expr → Expr
f :0 y  = y
f x  :0 = x
f x  y  = x + y

lemma :  ∀ {x y} → x ≢ :0 → y ≢ :0 → f x y ≡ x + y

lemma {:0}    {_}     e≢0 _    =  ⊥-elim (e≢0 PE.refl)
lemma {_}     {:0}    _   e'≢0 =  ⊥-elim (e'≢0 PE.refl)
lemma {_}     {_}     _   _    =  PE.refl                 -- I

{- II 
lemma {gen _} {gen _} _   _    =  PE.refl 
lemma {gen _} {_ + _} _   _    =  PE.refl     
lemma {_ + _} {gen _} _   _    =  PE.refl    
lemma {_ + _} {_ + _} _   _    =  PE.refl 
-}
---------------------------------------------------------------------------

Agda  reports  refl  in (I) as not sufficient. Why?

Each wildcard in (I) intends to denote any  x : Expr  which top
constructor is not  :0.
And all these cases (II) can be filled automatically by the type checker
in place of (I).
Am I missing something?
May be there is some keyword that switches such an automatic filling?

It may well happen that  Expr  has more binary constructors, for
example,  _*_ and  div.
Then the patterns for `lemma' will probably fill more that three pages
of text.

What is the way out?

Thanks,

------
Sergei