[Agda] "xs ≡ [] → " question

[Sergei Meshveliani]

Please, 
what is the most natural way to prove  g  below?

------------------------------------------------------
open import Data.Nat  using (ℕ)
open import Data.List using (List; []; _∷_)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

f : List ℕ  → ℕ
f []      =  1
f (_ ∷ _) =  0

postulate  ps : List ℕ

g : ps ≡ [] → f ps ≡ 1
g PE.refl =  PE.refl    -- is not type-checked
--------------------------------------------------------


I find the proof that uses

  lemma : ∀ {xs} → xs ≡ [] → f xs ≡ 1
  lemma PE.refl = PE.refl

But
1) why the same implementation rule does not work for  g ?
2) is there possible a simpler proof than by introducing  lemma ?

Thanks,

------
Sergei