title: Stuck in infinite inversion loop Coq
body: <p>I have an inductive relation as shown below titled <i> suffix</i>. I am trying to prove the related theorem <i> suffix_app</i>. My general idea is to use that fact that <i> suffix xs ys</i> to show that xs is either equal to ys or that it is some series of elements <i> cons</i>'d onto ys. </p>
  
  <pre><code>Require Import Coq.Lists.List.
  Import ListNotations.
  
  Inductive suffix {X : Type} : list X -&gt; list X -&gt; Prop :=
    | suffix_end : forall xs,
            suffix xs xs
    | suffix_step : forall x xs ys,
            suffix xs ys -&gt;
            suffix (x :: xs) ys.
  
  Theorem suffix_app : forall (X: Type) (x:X) (xs ys: list X),
    suffix xs ys -&gt; 
    exists ws, xs = ws ++ ys.
  Proof.
    intros.
    inversion H.
    - exists []. reflexivity.
    -
  </code></pre>
  
  <p>However, when I use inversion, there's no way of actually ever "arriving" to the term that is equal to ys. Hence, I am stuck at the point currently seen in the code.</p>