Goal:
    A : Type  H : ReflectEq A  l : list A  x : A  xs : list A
  ============================
   (is_prefix l (x :: xs)
    → l = [] ∨ ∃ l' : list A, l = x :: l' ∧ is_prefix l' xs)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrcase@0> $1 $2