Goal:
    A : Type  H : ReflectEq A
  ============================
   (∀ (l1 l2 : list A) (H := CoreTactics.block) (l3 l4 : list A),
      {| pr1 := l1; pr2 := l2 |} = {| pr1 := l3; pr2 := l4 |}
      → split_prefix l1 l2 = split_prefix l3 l4
        → let H0 := CoreTactics.block in
          let
          '(prefix, l1', l2') := split_prefix l3 l4 in
           l3 = prefix ++ l1' ∧ l4 = prefix ++ l2')


DEBUG:Going to execute:
<coq-equations.plugin::refine_ho@0> $1
DEBUG LTAC Evaluated term: (fun_elim ?P ?f ?f0 ?f3 ?f4)

Goals:
    A : Type  H : ReflectEq A
  ============================
   (∀ l2 : list A,
      (λ (l1 l3 : list A) (x : list A * list A * list A),
         ∀ (H := CoreTactics.block) (l4 l5 : list A),
           {| pr1 := l1; pr2 := l3 |} = {| pr1 := l4; pr2 := l5 |}
           → x = split_prefix l4 l5
             → let H0 := CoreTactics.block in
               let
               '(prefix, l1', l2') := split_prefix l4 l5 in
                l4 = prefix ++ l1' ∧ l5 = prefix ++ l2') [] l2 (
        [], [], l2))

    A : Type  H : ReflectEq A
  ============================
   (∀ (a : A) (l : list A),
      (λ (l1 l2 : list A) (x : list A * list A * list A),
         ∀ (H := CoreTactics.block) (l3 l4 : list A),
           {| pr1 := l1; pr2 := l2 |} = {| pr1 := l3; pr2 := l4 |}
           → x = split_prefix l3 l4
             → let H0 := CoreTactics.block in
               let
               '(prefix, l1', l2') := split_prefix l3 l4 in
                l3 = prefix ++ l1' ∧ l4 = prefix ++ l2') 
        (a :: l) [] ([], a :: l, []))

    A : Type  H : ReflectEq A
  ============================
   (∀ (a1 : A) (l1 : list A) (a2 : A) (l2 : list A),
      (λ (a3 : A) (l3 : list A) (a4 : A) (refine : bool) 
         (l4 : list A) (H0 : list A * list A * list A),
         (a3 == a4) = refine
         → (λ (l5 l6 : list A) (x : list A * list A * list A),
              ∀ (H := CoreTactics.block) (l7 l8 : list A),
                {| pr1 := l5; pr2 := l6 |} = {| pr1 := l7; pr2 := l8 |}
                → x = split_prefix l7 l8
                  → let H1 := CoreTactics.block in
                    let
                    '(prefix, l1', l2') := split_prefix l7 l8 in
                     l7 = prefix ++ l1' ∧ l8 = prefix ++ l2') 
             (a3 :: l3) (a4 :: l4) H0) a1 l1 a2 false l2
        ([], a1 :: l1, a2 :: l2))

    A : Type  H : ReflectEq A
  ============================
   (∀ (a1 : A) (l1 : list A) (a2 : A) (l2 prefix l1' l2' : list A),
      (λ (a3 : A) (l3 : list A) (a4 : A) (l4 : list A) 
         (refine H0 : list A * list A * list A),
         split_prefix l3 l4 = refine
         → (λ (l5 l6 : list A) (x : list A * list A * list A),
              ∀ (H := CoreTactics.block) (l7 l8 : list A),
                {| pr1 := l5; pr2 := l6 |} = {| pr1 := l7; pr2 := l8 |}
                → x = split_prefix l7 l8
                  → let H1 := CoreTactics.block in
                    let
                    '(prefix0, l1'0, l2'0) := split_prefix l7 l8 in
                     l7 = prefix0 ++ l1'0 ∧ l8 = prefix0 ++ l2'0) l3 l4
             (split_prefix l3 l4)
           → (λ (a5 : A) (l5 : list A) (a6 : A) (refine0 : bool) 
                (l6 : list A) (H1 : list A * list A * list A),
                (a5 == a6) = refine0
                → (λ (l7 l8 : list A) (x : list A * list A * list A),
                     ∀ (H := CoreTactics.block) (l9 l10 : list A),
                       {| pr1 := l7; pr2 := l8 |} =
                       {| pr1 := l9; pr2 := l10 |}
                       → x = split_prefix l9 l10
                         → let H2 := CoreTactics.block in
                           let
                           '(prefix0, l1'0, l2'0) := 
                            split_prefix l9 l10 in
                            l9 = prefix0 ++ l1'0 ∧ l10 = prefix0 ++ l2'0)
                    (a5 :: l5) (a6 :: l6) H1) a3 l3 a4 true l4 H0) a1 l1 a2
        l2 (prefix, l1', l2') (a1 :: prefix, l1', l2'))


DEBUG:Going to execute:
intros

Goals:
    A : Type  H : ReflectEq A  l2 : list A
  ============================
   ((λ (l1 l2 : list A) (x : list A * list A * list A),
       ∀ (H := CoreTactics.block) (l3 l4 : list A),
         {| pr1 := l1; pr2 := l2 |} = {| pr1 := l3; pr2 := l4 |}
         → x = split_prefix l3 l4
           → let H0 := CoreTactics.block in
             let
             '(prefix, l1', l2') := split_prefix l3 l4 in
              l3 = prefix ++ l1' ∧ l4 = prefix ++ l2') [] l2 (
      [], [], l2))

    A : Type  H : ReflectEq A  a : A  l : list A
  ============================
   ((λ (l1 l2 : list A) (x : list A * list A * list A),
       ∀ (H := CoreTactics.block) (l3 l4 : list A),
         {| pr1 := l1; pr2 := l2 |} = {| pr1 := l3; pr2 := l4 |}
         → x = split_prefix l3 l4
           → let H0 := CoreTactics.block in
             let
             '(prefix, l1', l2') := split_prefix l3 l4 in
              l3 = prefix ++ l1' ∧ l4 = prefix ++ l2') 
      (a :: l) [] ([], a :: l, []))

    A : Type  H : ReflectEq A  a1 : A  l1 : list A  a2 : A  l2 : list A
  ============================
   ((λ (a1 : A) (l1 : list A) (a2 : A) (refine : bool) 
       (l2 : list A) (H0 : list A * list A * list A),
       (a1 == a2) = refine
       → (λ (l3 l4 : list A) (x : list A * list A * list A),
            ∀ (H := CoreTactics.block) (l5 l6 : list A),
              {| pr1 := l3; pr2 := l4 |} = {| pr1 := l5; pr2 := l6 |}
              → x = split_prefix l5 l6
                → let H1 := CoreTactics.block in
                  let
                  '(prefix, l1', l2') := split_prefix l5 l6 in
                   l5 = prefix ++ l1' ∧ l6 = prefix ++ l2') 
           (a1 :: l1) (a2 :: l2) H0) a1 l1 a2 false l2
      ([], a1 :: l1, a2 :: l2))

  
  A : Type
  H : ReflectEq A
  a1 : A
  l1 : list A
  a2 : A
  l2 : list A
  prefix : list A
  l1' : list A
  l2' : list A
  ============================
   ((λ (a1 : A) (l1 : list A) (a2 : A) (l2 : list A) 
       (refine H0 : list A * list A * list A),
       split_prefix l1 l2 = refine
       → (λ (l3 l4 : list A) (x : list A * list A * list A),
            ∀ (H := CoreTactics.block) (l5 l6 : list A),
              {| pr1 := l3; pr2 := l4 |} = {| pr1 := l5; pr2 := l6 |}
              → x = split_prefix l5 l6
                → let H1 := CoreTactics.block in
                  let
                  '(prefix, l1', l2') := split_prefix l5 l6 in
                   l5 = prefix ++ l1' ∧ l6 = prefix ++ l2') l1 l2
           (split_prefix l1 l2)
         → (λ (a3 : A) (l3 : list A) (a4 : A) (refine0 : bool) 
              (l4 : list A) (H1 : list A * list A * list A),
              (a3 == a4) = refine0
              → (λ (l5 l6 : list A) (x : list A * list A * list A),
                   ∀ (H := CoreTactics.block) (l7 l8 : list A),
                     {| pr1 := l5; pr2 := l6 |} = {| pr1 := l7; pr2 := l8 |}
                     → x = split_prefix l7 l8
                       → let H2 := CoreTactics.block in
                         let
                         '(prefix, l1', l2') := split_prefix l7 l8 in
                          l7 = prefix ++ l1' ∧ l8 = prefix ++ l2') 
                  (a3 :: l3) (a4 :: l4) H1) a1 l1 a2 true l2 H0) a1 l1 a2 l2
      (prefix, l1', l2') (a1 :: prefix, l1', l2'))


DEBUG:Going to execute:
cbv beta

Goals:
    A : Type  H : ReflectEq A  l2 : list A
  ============================
   (∀ (H := CoreTactics.block) (l1 l3 : list A),
      {| pr1 := []; pr2 := l2 |} = {| pr1 := l1; pr2 := l3 |}
      → ([], [], l2) = split_prefix l1 l3
        → let H0 := CoreTactics.block in
          let
          '(prefix, l1', l2') := split_prefix l1 l3 in
           l1 = prefix ++ l1' ∧ l3 = prefix ++ l2')

    A : Type  H : ReflectEq A  a : A  l : list A
  ============================
   (∀ (H := CoreTactics.block) (l1 l2 : list A),
      {| pr1 := a :: l; pr2 := [] |} = {| pr1 := l1; pr2 := l2 |}
      → ([], a :: l, []) = split_prefix l1 l2
        → let H0 := CoreTactics.block in
          let
          '(prefix, l1', l2') := split_prefix l1 l2 in
           l1 = prefix ++ l1' ∧ l2 = prefix ++ l2')

    A : Type  H : ReflectEq A  a1 : A  l1 : list A  a2 : A  l2 : list A
  ============================
   ((a1 == a2) = false
    → ∀ (H := CoreTactics.block) (l3 l4 : list A),
        {| pr1 := a1 :: l1; pr2 := a2 :: l2 |} = {| pr1 := l3; pr2 := l4 |}
        → ([], a1 :: l1, a2 :: l2) = split_prefix l3 l4
          → let H0 := CoreTactics.block in
            let
            '(prefix, l1', l2') := split_prefix l3 l4 in
             l3 = prefix ++ l1' ∧ l4 = prefix ++ l2')

  
  A : Type
  H : ReflectEq A
  a1 : A
  l1 : list A
  a2 : A
  l2 : list A
  prefix : list A
  l1' : list A
  l2' : list A
  ============================
   (split_prefix l1 l2 = (prefix, l1', l2')
    → (∀ (H := CoreTactics.block) (l3 l4 : list A),
         {| pr1 := l1; pr2 := l2 |} = {| pr1 := l3; pr2 := l4 |}
         → split_prefix l1 l2 = split_prefix l3 l4
           → let H0 := CoreTactics.block in
             let
             '(prefix, l1', l2') := split_prefix l3 l4 in
              l3 = prefix ++ l1' ∧ l4 = prefix ++ l2')
      → (a1 == a2) = true
        → ∀ (H := CoreTactics.block) (l3 l4 : list A),
            {| pr1 := a1 :: l1; pr2 := a2 :: l2 |} =
            {| pr1 := l3; pr2 := l4 |}
            → (a1 :: prefix, l1', l2') = split_prefix l3 l4
              → let H0 := CoreTactics.block in
                let
                '(prefix, l1', l2') := split_prefix l3 l4 in
                 l3 = prefix ++ l1' ∧ l4 = prefix ++ l2')


DEBUG:Going to execute:
DepElim.simplify_dep_elim

Goals:
    A : Type  H : ReflectEq A  l2 : list A
  ============================
   (∀ (H := CoreTactics.block) (l1 l3 : list A),
      {| pr1 := []; pr2 := l2 |} = {| pr1 := l1; pr2 := l3 |}
      → ([], [], l2) = split_prefix l1 l3
        → let H0 := CoreTactics.block in
          let
          '(prefix, l1', l2') := split_prefix l1 l3 in
           l1 = prefix ++ l1' ∧ l3 = prefix ++ l2')

    A : Type  H : ReflectEq A  a : A  l : list A
  ============================
   (∀ (H := CoreTactics.block) (l1 l2 : list A),
      {| pr1 := a :: l; pr2 := [] |} = {| pr1 := l1; pr2 := l2 |}
      → ([], a :: l, []) = split_prefix l1 l2
        → let H0 := CoreTactics.block in
          let
          '(prefix, l1', l2') := split_prefix l1 l2 in
           l1 = prefix ++ l1' ∧ l2 = prefix ++ l2')

    A : Type  H : ReflectEq A  a1 : A  l1 : list A  a2 : A  l2 : list A
  ============================
   ((a1 == a2) = false
    → ∀ (H := CoreTactics.block) (l3 l4 : list A),
        {| pr1 := a1 :: l1; pr2 := a2 :: l2 |} = {| pr1 := l3; pr2 := l4 |}
        → ([], a1 :: l1, a2 :: l2) = split_prefix l3 l4
          → let H0 := CoreTactics.block in
            let
            '(prefix, l1', l2') := split_prefix l3 l4 in
             l3 = prefix ++ l1' ∧ l4 = prefix ++ l2')

  
  A : Type
  H : ReflectEq A
  a1 : A
  l1 : list A
  a2 : A
  l2 : list A
  prefix : list A
  l1' : list A
  l2' : list A
  ============================
   (split_prefix l1 l2 = (prefix, l1', l2')
    → (∀ (H := CoreTactics.block) (l3 l4 : list A),
         {| pr1 := l1; pr2 := l2 |} = {| pr1 := l3; pr2 := l4 |}
         → split_prefix l1 l2 = split_prefix l3 l4
           → let H0 := CoreTactics.block in
             let
             '(prefix, l1', l2') := split_prefix l3 l4 in
              l3 = prefix ++ l1' ∧ l4 = prefix ++ l2')
      → (a1 == a2) = true
        → ∀ (H := CoreTactics.block) (l3 l4 : list A),
            {| pr1 := a1 :: l1; pr2 := a2 :: l2 |} =
            {| pr1 := l3; pr2 := l4 |}
            → (a1 :: prefix, l1', l2') = split_prefix l3 l4
              → let H0 := CoreTactics.block in
                let
                '(prefix, l1', l2') := split_prefix l3 l4 in
                 l3 = prefix ++ l1' ∧ l4 = prefix ++ l2')


DEBUG:Going to execute:
repeat DepElim.simplify_one_dep_elim