Require Import Program Arith.

Program Fixpoint foo (n: nat) : Prop :=
    match n with
    | O => True
    | S p => match Nat.eqb p 0 with true => _ | false => _ end
    end.

Next Obligation. (* Has Heq_anonymous: true = (p =? 0) *)

Program Fixpoint foo (n: nat) : Prop :=
    match n with
    | O => True
    | S p => if eq_nat_dec p 0 then _ else _
    end.

Next Obligation. (* Doesn't have Heq_anonymous *)