∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1)
  (step : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n)) (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))) (id : ℕ) (rupHints : Array ℕ),
  step = some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) →
    (match step with
      | none => h_1 ()
      | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
      | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
      | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
      | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) ≍
      h_2 id rupHints