Bug: f_unfold obligation after Defined

[quimFIB]

Coming from this topic on zulip, I've built a smaller example:

Equations example {T : Type} (s : seq T) : seq T
  by wf (seq.size s) lt :=
  example [::] := [::];
  example (x::xs) := foldl foo [::] [::]
where foo (acc : (seq T)) (x0 : T) : seq T :=
  foo acc x0 := acc.

This defintion yields a warning

Warning: Solve Obligations tactic returned error: Found no subterm matching
"example_clause_2_foo (fun (x : Type) (x0 : seq x) => fun=> example x0) ?M3534 ?M3535"
in the current goal.

Which makes the compilation fail when trying to compile this code from the command line with the following error:

Error: Unsolved obligations when closing file ./theories/extract.v:
have unsolved obligations.

I am using coq-8.20 and coq-equations v1.3.1-8.20 built from source. Should it be needed I attach a dump of my opam list.
opam-list.txt