Missing equality hypothesis in proof obligation?

[fpottier]

trafficstars

Hello! I am trying to define a function by well-founded recursion (using Equations ... by wf). The definition involves a with node. There is a recursive call inside the with node, and to prove that this recursive call is decreasing, an equation is needed: one must exploit the fact that the scrutinee and the pattern (of the with node) are equal. Yet this equation does not appear as a hypothesis in the proof obligation, as I would expect. Here is a simplified example:

From Coq.Unicode Require Import Utf8.
From Equations Require Import Equations.

Definition state : Type :=
  nat.

Definition result : Type :=
  nat.

Inductive choice : Type :=
| Continue : state  → choice
| Finished : result → choice.

Definition evolve (s : state) : choice :=
  match s with
  | 0 =>   Finished 0
  | S s => Continue s
  end.

Equations loop (st : state) : result
by wf st lt :=
loop st with evolve st => {
  | (Continue st') := loop st'
  | (Finished x)   := x
}.
Next Obligation.
  clear loop.
  (* This obligation is not provable. *)
  (* The proof obligation is [st' < st], with no hypotheses. *)
  (* The hypothesis [evolve st = Continue st'] is missing. *)
Abort.

Is this a bug, or is this behavior intended?

Am I expected to give evolve a dependent type to reflect the fact that evolve st = Continue st' implies lt st' st? That might work, but it seems a pity to impose this extra burden on the user.