Goal:
    A : Type  H : ReflectEq A  l1 : list A  l2 : list A
  ============================
   ((let
     '(prefix, l1', l2') := split_prefix (rev l1) (rev l2) in
      rev l1 = prefix ++ l1' ∧ rev l2 = prefix ++ l2')
    → let
      '(l1', l2', suffix) :=
       let
       '(suffix, l1, l2) := split_prefix (rev l1) (rev l2) in
        (rev l1, rev l2, rev suffix) in
       l1 = l1' ++ suffix ∧ l2 = l2' ++ suffix)


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