Goal:
  
  A : Type
  H : ReflectEq A
  l1 : list A
  l2 : list A
  y : 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.ltac::revert@0> $1
DEBUG LTAC Evaluated term: (split_prefix_is_prefix (rev l1) (rev l2))