Parameter X : Type.
Parameter f : X -> bool.
Parameter x : X.

Inductive gRel : X -> bool -> Prop :=
  | is_x : gRel x true
  | is_not_x : forall y: X, y <> x -> gRel y (f y)
.

Definition gdec (h: forall a b: X, {a = b}+{a <> b}) : X -> bool :=
  fun a => if h a x then true else f a.

Lemma gRel_is_a_fun: (forall a b: X, {a = b}+{a <> b}) ->
  exists g : X -> bool, forall a, gRel a (g a).
Proof.
intro hdec.
exists (gdec hdec); unfold gdec.
intro a; destruct (hdec a x).
now subst; apply is_x.
now apply is_not_x.
Qed.