[Agda] explicit irrelevance

[Sergei Meshveliani]

People,
I am trying to replace the  irrelevance annotations  
with explicit irrelevance axioms ans proofs.
Consider the example:

-----------------------------------------------------------------
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 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 =  case x ≟ 0# of \ { (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 =
                 case x ≟ 0#
                 of \
                 { (yes x=0) → ⊥-elim (x≉0 x=0)
                 ; (no x/=0) → 
                               ??
                 }
----------------------------------------------------------------- 

Here  irrel-f  is used instead of the irrelevance annotation  
.(¬ x ≈ 0#)  in the signature for f.

And I need to prove  g=f-if.

≈refl  does not work. This is probably because there is no witness for
that  x≉0   and a value in  ¬ x ≈ 0#  used in the definition for  g  are
the same values.
For example, using  irrel-f  proves   f x x≉0 ≈ f x x/=0  
(in the context of `??'). 
But I do not see how to move it to  g.

Can anybody demonstrate a proof?

Thanks,

------
Sergei