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


DEBUG:Going to execute:
left