Goal:
    A : Type  H : ReflectEq A  x : A  xs : list A  y : A  ys : list A
  ============================
   (is_prefix (x :: xs) (y :: ys) → x = y ∧ is_prefix xs ys)


DEBUG:Going to execute:
move  =>[tl [=-> ->]]