[Agda] uniform normalization

[Sergei Meshveliani]

Hello, All.

I have the following question.
The program

-------------------------------------------------
open import Relation.Binary.PropositionalEquality
open import Data.Nat

f : ℕ → ℕ
f 0       = 0
f (suc _) = 0

theorem :  ∀ n → f n ≡ 0
theorem _ =  refl
--------------------------------------------------

is not type-checked, because Agda expects the two proofs to be given.
One for the case 0, another for the case (suc _). 
Both proofs can be set `refl', that is -- by normalization.

Could the type checker check the proof by a single `refl', by
normalizing each branch?
(this will simplify many proofs).

Thanks,

------
Sergei