`zify` incorrectly uses `Eq.refl`

In Lean 3 we had:
```
import tactic.zify

example (h : 0 = 0) : true :=
begin
  zify at h,     -- `h` is `(0 : ℤ) = 0`, not `true`.
  fail_if_success { assumption, },
  trivial,
end
```
but in Lean 4 we now have:
```
import Mathlib.Tactic.Zify

example (h : 0 = 0) : True := by
  zify at h   -- `h` has become `True`
  assumption
```