∀ {n : ℕ} (assignments0 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (assignments0_size : assignments0.size = n)
  (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n)
  (i : Fin n) (j : Fin units.size) (i_gt_zero : ↑i > 0)
  (motive :
    (b : Bool) →
      Bool →
        units[↑j] = (⟨↑i, ⋯⟩, b) →
          assignments[↑i] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment b assignments0[↑i] →
            Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b assignments0[↑i] = false → Prop)
  (b x : Bool) (h1 : units[↑j] = (⟨↑i, ⋯⟩, b))
  (h2 : assignments[↑i] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment b assignments0[↑i])
  (h3 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b assignments0[↑i] = false),
  (∀ (h1 : units[↑j] = (⟨↑i, ⋯⟩, true))
      (h2 : assignments[↑i] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment true assignments0[↑i])
      (h3 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment true assignments0[↑i] = false),
      b = true → x = true → motive true true h1 h2 h3) →
    (∀ (h1 : units[↑j] = (⟨↑i, ⋯⟩, true))
        (h2 : assignments[↑i] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment true assignments0[↑i])
        (h3 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment true assignments0[↑i] = false),
        b = true → x = false → motive true false h1 h2 h3) →
      (∀ (h1 : units[↑j] = (⟨↑i, ⋯⟩, false))
          (h2 : assignments[↑i] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment false assignments0[↑i])
          (h3 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment false assignments0[↑i] = false),
          b = false → x = true → motive false true h1 h2 h3) →
        (∀ (h1 : units[↑j] = (⟨↑i, ⋯⟩, false))
            (h2 : assignments[↑i] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment false assignments0[↑i])
            (h3 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment false assignments0[↑i] = false),
            b = false → x = false → motive false false h1 h2 h3) →
          motive b x h1 h2 h3