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:
case : l x xs  => [|y ys ? ? [tl [=-> ->]]]