[Agda] explicit irrelevance question

[Sergei Meshveliani]

Dear Agda developers,

can you, please tell whether the below statement  g=f-if
must have a proof in Agda ?
If yes, then what can be a proof ?

(I am stuck with both explicit irrelevance and a dot-annotated
irrelevance). 

Thanks,

------
Sergei


--------------------------------------------------------------
open import Level            using (_⊔_)
open import Function         using (case_of_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary  using (module IsEquivalence;
                                    module DecSetoid; DecSetoid)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Empty using (⊥-elim)


module _ {α α=} (A : DecSetoid α α=) (0# : DecSetoid.Carrier A)
  where
  open DecSetoid A using (_≈_; _≟_; isEquivalence)
                                    renaming (Carrier to C)
  open IsEquivalence isEquivalence renaming (refl to ≈refl)

  record Foo : Set (α ⊔ α=)
    where
    field f       : (x : C) → ¬ x ≈ 0# → C
          irrel-f : (x : C) → (nz nz' : ¬ x ≈ 0#) → f x nz ≈ f x nz'

    g : C → C
    g x  with x ≟ 0#
    ...             | yes _  = x
    ...             | no x≉0 = f x x≉0

    g=f-if : ∀ x → (x≉0 : ¬ x ≈ 0#) → g x ≈ f x x≉0
    g=f-if x x≉0  with x ≟ 0#
    ...                      | yes x=0 = ⊥-elim (x≉0 x=0)
    ...                      | no x/=0 = ≈refl
                                         -- ?
-----------------------------------------------------------------