∀ {α : Type u_1}
  (motive :
    (x x_1 x_2 x_3 : List (α × Bool)) →
      (x_4 : α) →
        (x_5 : Bool) →
          (x_6 : α) →
            (x_7 : Bool) → x ++ (x_4, x_5) :: (x_4, !x_5) :: x_1 = x_2 ++ (x_6, x_7) :: (x_6, !x_7) :: x_3 → Prop)
  (x x_1 x_2 x_3 : List (α × Bool)) (x_4 : α) (x_5 : Bool) (x_6 : α) (x_7 : Bool)
  (x_8 : x ++ (x_4, x_5) :: (x_4, !x_5) :: x_1 = x_2 ++ (x_6, x_7) :: (x_6, !x_7) :: x_3),
  (∀ (x x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool)
      (H : [] ++ (x_10, x_11) :: (x_10, !x_11) :: x = [] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9),
      motive [] x [] x_9 x_10 x_11 x_12 x_13 H) →
    (∀ (x : List (α × Bool)) (x3 : α) (b3 : Bool) (x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α)
        (x_13 : Bool)
        (H : [] ++ (x_10, x_11) :: (x_10, !x_11) :: x = [(x3, b3)] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9),
        motive [] x [(x3, b3)] x_9 x_10 x_11 x_12 x_13 H) →
      (∀ (x3 : α) (b3 : Bool) (x x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α) (x_13 : Bool)
          (H : [(x3, b3)] ++ (x_10, x_11) :: (x_10, !x_11) :: x = [] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9),
          motive [(x3, b3)] x [] x_9 x_10 x_11 x_12 x_13 H) →
        (∀ (x : List (α × Bool)) (x3 : α) (b3 : Bool) (x4 : α) (b4 : Bool) (tl x_9 : List (α × Bool)) (x_10 : α)
            (x_11 : Bool) (x_12 : α) (x_13 : Bool)
            (H :
              [] ++ (x_10, x_11) :: (x_10, !x_11) :: x =
                (x3, b3) :: (x4, b4) :: tl ++ (x_12, x_13) :: (x_12, !x_13) :: x_9),
            motive [] x ((x3, b3) :: (x4, b4) :: tl) x_9 x_10 x_11 x_12 x_13 H) →
          (∀ (x3 : α) (b3 : Bool) (x4 : α) (b4 : Bool) (tl x x_9 : List (α × Bool)) (x_10 : α) (x_11 : Bool) (x_12 : α)
              (x_13 : Bool)
              (H :
                (x3, b3) :: (x4, b4) :: tl ++ (x_10, x_11) :: (x_10, !x_11) :: x =
                  [] ++ (x_12, x_13) :: (x_12, !x_13) :: x_9),
              motive ((x3, b3) :: (x4, b4) :: tl) x [] x_9 x_10 x_11 x_12 x_13 H) →
            (∀ (x3 : α) (b3 : Bool) (tl x : List (α × Bool)) (x4 : α) (b4 : Bool) (tl2 x_9 : List (α × Bool)) (x_10 : α)
                (x_11 : Bool) (x_12 : α) (x_13 : Bool)
                (H :
                  (x3, b3) :: tl ++ (x_10, x_11) :: (x_10, !x_11) :: x =
                    (x4, b4) :: tl2 ++ (x_12, x_13) :: (x_12, !x_13) :: x_9),
                motive ((x3, b3) :: tl) x ((x4, b4) :: tl2) x_9 x_10 x_11 x_12 x_13 H) →
              motive x x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8