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


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 l : list A),
           {| pr1 := l1; pr2 := l3 |} = {| pr1 := l4; pr2 := l5 |}
           → x = split_prefix l4 l5
             → let H0 := CoreTactics.block in
               is_prefix l l4
               → is_prefix l l5
                 → is_prefix l (fst (fst (split_prefix l4 l5)))) [] 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 l0 : list A),
           {| pr1 := l1; pr2 := l2 |} = {| pr1 := l3; pr2 := l4 |}
           → x = split_prefix l3 l4
             → let H0 := CoreTactics.block in
               is_prefix l0 l3
               → is_prefix l0 l4
                 → is_prefix l0 (fst (fst (split_prefix l3 l4)))) 
        (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 l : list A),
                {| pr1 := l5; pr2 := l6 |} = {| pr1 := l7; pr2 := l8 |}
                → x = split_prefix l7 l8
                  → let H1 := CoreTactics.block in
                    is_prefix l l7
                    → is_prefix l l8
                      → is_prefix l (fst (fst (split_prefix l7 l8))))
             (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 l : list A),
                {| pr1 := l5; pr2 := l6 |} = {| pr1 := l7; pr2 := l8 |}
                → x = split_prefix l7 l8
                  → let H1 := CoreTactics.block in
                    is_prefix l l7
                    → is_prefix l l8
                      → is_prefix l (fst (fst (split_prefix l7 l8)))) 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 l : list A),
                       {| pr1 := l7; pr2 := l8 |} =
                       {| pr1 := l9; pr2 := l10 |}
                       → x = split_prefix l9 l10
                         → let H2 := CoreTactics.block in
                           is_prefix l l9
                           → is_prefix l l10
                             → is_prefix l (fst (fst (split_prefix l9 l10))))
                    (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 l : list A),
         {| pr1 := l1; pr2 := l2 |} = {| pr1 := l3; pr2 := l4 |}
         → x = split_prefix l3 l4
           → let H0 := CoreTactics.block in
             is_prefix l l3
             → is_prefix l l4 → is_prefix l (fst (fst (split_prefix l3 l4))))
      [] 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 l : list A),
         {| pr1 := l1; pr2 := l2 |} = {| pr1 := l3; pr2 := l4 |}
         → x = split_prefix l3 l4
           → let H0 := CoreTactics.block in
             is_prefix l l3
             → is_prefix l l4 → is_prefix l (fst (fst (split_prefix l3 l4))))
      (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 l : list A),
              {| pr1 := l3; pr2 := l4 |} = {| pr1 := l5; pr2 := l6 |}
              → x = split_prefix l5 l6
                → let H1 := CoreTactics.block in
                  is_prefix l l5
                  → is_prefix l l6
                    → is_prefix l (fst (fst (split_prefix l5 l6))))
           (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 l : list A),
              {| pr1 := l3; pr2 := l4 |} = {| pr1 := l5; pr2 := l6 |}
              → x = split_prefix l5 l6
                → let H1 := CoreTactics.block in
                  is_prefix l l5
                  → is_prefix l l6
                    → is_prefix l (fst (fst (split_prefix l5 l6)))) 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 l : list A),
                     {| pr1 := l5; pr2 := l6 |} = {| pr1 := l7; pr2 := l8 |}
                     → x = split_prefix l7 l8
                       → let H2 := CoreTactics.block in
                         is_prefix l l7
                         → is_prefix l l8
                           → is_prefix l (fst (fst (split_prefix l7 l8))))
                  (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 l : list A),
      {| pr1 := []; pr2 := l2 |} = {| pr1 := l1; pr2 := l3 |}
      → ([], [], l2) = split_prefix l1 l3
        → let H0 := CoreTactics.block in
          is_prefix l l1
          → is_prefix l l3 → is_prefix l (fst (fst (split_prefix l1 l3))))

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

    A : Type  H : ReflectEq A  a1 : A  l1 : list A  a2 : A  l2 : list A
  ============================
   ((a1 == a2) = false
    → ∀ (H := CoreTactics.block) (l3 l4 l : 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
            is_prefix l l3
            → is_prefix l l4 → is_prefix l (fst (fst (split_prefix l3 l4))))

  
  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 l : list A),
         {| pr1 := l1; pr2 := l2 |} = {| pr1 := l3; pr2 := l4 |}
         → split_prefix l1 l2 = split_prefix l3 l4
           → let H0 := CoreTactics.block in
             is_prefix l l3
             → is_prefix l l4 → is_prefix l (fst (fst (split_prefix l3 l4))))
      → (a1 == a2) = true
        → ∀ (H := CoreTactics.block) (l3 l4 l : 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
                is_prefix l l3
                → is_prefix l l4
                  → is_prefix l (fst (fst (split_prefix l3 l4))))


DEBUG:Going to execute:
DepElim.simplify_dep_elim

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

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

    A : Type  H : ReflectEq A  a1 : A  l1 : list A  a2 : A  l2 : list A
  ============================
   ((a1 == a2) = false
    → ∀ (H := CoreTactics.block) (l3 l4 l : 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
            is_prefix l l3
            → is_prefix l l4 → is_prefix l (fst (fst (split_prefix l3 l4))))

  
  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 l : list A),
         {| pr1 := l1; pr2 := l2 |} = {| pr1 := l3; pr2 := l4 |}
         → split_prefix l1 l2 = split_prefix l3 l4
           → let H0 := CoreTactics.block in
             is_prefix l l3
             → is_prefix l l4 → is_prefix l (fst (fst (split_prefix l3 l4))))
      → (a1 == a2) = true
        → ∀ (H := CoreTactics.block) (l3 l4 l : 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
                is_prefix l l3
                → is_prefix l l4
                  → is_prefix l (fst (fst (split_prefix l3 l4))))


DEBUG:Going to execute:
repeat DepElim.simplify_one_dep_elim