Why does Program Fixpoint leave behind a temporary_proof2_subproof axiom in this example?

Question

I have reduced my development into the following minimal reproducer:

From Coq Require Import Lists.List. Import ListNotations.
From Coq Require Import Program.Tactics.
From Coq Require Import Program.Wf.
From Coq Require Import ZArith.
From Coq Require Import Lia.
Set Default Goal Selector "!".

Inductive segment := Repeat (xs : list nat) | Symbol (x : nat).

Definition strip_sym_prefix (s : list nat) (u : list segment)
    : {u' | u = map Symbol s ++ u'} + {True}.
Admitted.

Lemma length_gt0_if_not_nil : forall A (xs : list A),
  [] <> xs -> length xs <> 0.
Proof. intros A xs H Hlen. apply length_zero_iff_nil in Hlen. auto. Qed.

Local Ltac Zify.zify_pre_hook ::=
  lazymatch goal with
  | H: [] = _ -> False |- _ => apply length_gt0_if_not_nil in H
  | _ => idtac
  end.

Local Obligation Tactic := program_simplify; autorewrite with list; intuition.

Program Fixpoint subsumes (t : list segment) (u : list segment)
    {measure (length t + length u)} : bool :=
  match u with
  | Repeat s :: u =>
    match s with
    | [] => subsumes t u
    | _ =>
      match strip_sym_prefix s t with
      | inleft (exist _ t' _) => subsumes t' (Repeat s :: u)
      | inright _ => false
      end
    end
  | _ => false
  end.

Now, Print Assumptions subsumes. only lists strip_sym_prefix as an axiom, as I would expect. However, if we run coqchk:

$ coqc --version
The Coq Proof Assistant, version 8.16.1
compiled with OCaml 4.14.0
$ coqc Repro.v
$ coqchk -silent -o -norec Repro.vo

CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms:
    Coq.ssr.ssrunder.Under_rel.Over_rel
    Coq.ssr.ssrunder.Under_rel.Under_rel_from_rel
    Coq.ssr.ssrunder.Under_rel.over_rel
    Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
    Coq.ssr.ssrunder.Under_rel.over_rel_done
    Coq.ssr.ssrunder.Under_rel.Under_rel
    Coq.ssr.ssrunder.Under_rel.Under_relE
    Repro.strip_sym_prefix
    Repro.temporary_proof2_subproof                        <-- ???
    Coq.ssr.ssrunder.Under_rel.under_rel_done

* Constants/Inductives relying on type-in-type: <none>

* Constants/Inductives relying on unsafe (co)fixpoints: <none>

* Inductives whose positivity is assumed: <none>

As you can see, there is a stray axiom called temporary_proof2_subproof:

temporary_proof2_subproof
     : forall (s : list nat) (t' : list segment),
       ([] = s -> False) -> length t' < length s + length t'

Apart from coqchk, the extraction mechanism complains about it when I try to extract subsumes.

Some observations:

• the axiom can be proven by lia.

• I can make the superfluous axiom disappear, if instead of

  Local Obligation Tactic := program_simplify; autorewrite with list; intuition.
  

  I set the obligation tactic to idtac and then apply the above to each obligation manually:

  Obligation 1. program_simplify; autorewrite with list; intuition. Qed.
  Obligation 2. program_simplify; autorewrite with list; intuition. Qed.
  Obligation 3. program_simplify; autorewrite with list; intuition. Qed.
  Obligation 4. program_simplify; autorewrite with list; intuition. Qed.
  Obligation 5. program_simplify; autorewrite with list; intuition. Qed.
  Obligation 6. program_simplify; autorewrite with list; intuition. Qed.
  

To me at least, this is very surprising behavior. I do not understand what is going on. Is it a bug? How can I eliminate this axiom from my proof?