Indeed, it holds:

Definition id_at { X : Set } ( x : X ) := x = x.
Definition id_at_eq_refl { X : Set } { x : X } ( p : x = x ) := existT id_at x p = existT id_at x eq_refl.
Proposition id_at_eq_refl_uip { X : Set } { x : X }
  : (forall (p : x = x), id_at_eq_refl p)
    -> (forall (p : x = x), p = eq_refl).
Proof.
  intros H p.
  specialize (H p). unfold id_at_eq_refl in H.
  assert (projT2 (existT id_at x eq_refl) = @eq_refl _ (projT1 (existT id_at x eq_refl))) as Heqr by reflexivity.
  revert H Heqr.
  generalize (existT id_at x eq_refl) as k.
  intros k. intros <-. simpl. easy.
Qed.

The reason it works is interesting. We can generalize existT id_at x eq_refl, but still remember that its second component was eq_refl, because the type of projT2 k and eq_refl (on projT1 k) are the same (namely, id_at). Therefore, the first equality becomes usable (using an equality here usually means that you have to have the right-hand side be an unconstrained variable), so we can replace an eq_refl by p but still remember that it was eq_refl before, giving us p = eq_refl.

Indeed, it holds:

Definition id_at { X : Set } ( x : X ) := x = x.
Definition id_at_eq_refl { X : Set } { x : X } ( p : x = x ) := existT id_at x p = existT id_at x eq_refl.
Proposition id_at_eq_refl_uip { X : Set } { x : X }
  : (forall (p : x = x), id_at_eq_refl p)
    -> (forall (p : x = x), p = eq_refl).
Proof.
  intros H p.
  specialize (H p). unfold id_at_eq_refl in H.
  assert (projT2 (existT id_at x eq_refl) = @eq_refl _ (projT1 (existT id_at x eq_refl))) as Heqr by reflexivity.
  revert H Heqr.
  generalize (existT id_at x eq_refl) as k.
  intros k. intros <-. simpl. easy.
Qed.

The reason it works is interesting. We can generalize existT id_at x eq_refl as k, but still remember that its second component was eq_refl, because the type of projT2 k and eq_refl (on projT1 k) are the same (namely, id_at). Therefore, the first equality becomes usable (using an equality here usually means that you have to have the right-hand side be an unconstrained variable), so we can replace an eq_refl by p but still remember that it was eq_refl before, giving us p = eq_refl.