{α : Type u_1} →
  {β : Type u_2} →
    (motive : List (Std.Tactic.BVDecide.LRAT.Action β α) → Sort u_3) →
      (prf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
        (Unit → motive []) →
          ((id : ℕ) →
              (rupHints : Array ℕ) →
                (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                  motive (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail)) →
            ((id : ℕ) →
                (c : β) →
                  (rupHints : Array ℕ) →
                    (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                      motive (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf)) →
              ((id : ℕ) →
                  (c : β) →
                    (pivot : Std.Sat.Literal α) →
                      (rupHints : Array ℕ) →
                        (ratHints : Array (ℕ × Array ℕ)) →
                          (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                            motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf)) →
                ((ids : Array ℕ) →
                    (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                      motive (Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf)) →
                  motive prf