Coq не генерирует индуктивную гипотезу

Мне дали решение следующей теоремы, как показано ниже:

Require Import Coq.Lists.List.
Import ListNotations.

Inductive suffix {X : Type} : list X -> list X -> Prop :=
  | suffix_end : forall xs,
          suffix xs xs
  | suffix_step : forall x xs ys,
          suffix xs ys ->
          suffix (x :: xs) ys.

Theorem suffix_app (X: Type) (xs ys: list X) :
  suffix xs ys -> exists ws, xs = ws ++ ys.
Proof.
  induction 1 as [|x xsp ysp hs [zs zeq]]. 
  - exists []. reflexivity.
  - now exists (x :: zs); rewrite zeq.
Qed.

Я пытался быстро воспроизвести это на другой машине и попытался сделать это следующим образом:

Theorem suffix_app (X: Type) (xs ys: list X) :
  suffix xs ys -> exists ws, xs = ws ++ ys.
Proof.
  induction 1.
  - exists []. reflexivity.
  - (* Stuck here! *)
Abort.

то есть без предложения "как". Однако я застреваю из-за того, что автоматически названный эквивалент «zeq» не создается по причинам, которые я не могу понять. Почему здесь нет (автоматически названного) эквивалента «zeq», сгенерированного Coq во втором случае?