Goal:
  
  A : Type
  H : ReflectEq A
  a1 : A
  a2 : A
  prefix : list A
  l1' : list A
  l2' : list A
  Heq : split_prefix (prefix ++ l1') (prefix ++ l2') = (prefix, l1', l2')
  Heq0 : (a1 == a2) = true
  Heqcall : (a1 :: prefix, l1', l2') =
            split_prefix (a1 :: prefix ++ l1') (a2 :: prefix ++ l2')
  ============================
   (a1 :: prefix ++ l1' = (a1 :: prefix) ++ l1')


DEBUG:Going to execute:
solve
[ trivial
with eq_true
| reflexivity
| symmetry; trivial
| contradiction
| congruence ]