∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : DecidableEq α]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ]
  [inst_3 : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f →
      ∀ (c : β) (pivot : Std.Sat.Literal α) (f' : σ) (rupHints : Array ℕ) (ratHints : Array (ℕ × Array ℕ)),
        Std.Tactic.BVDecide.LRAT.Internal.Limplies α pivot c →
          Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd f c pivot rupHints ratHints = (f', true) →
            ∀ (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)),
              (∀ a ∈ restPrf, Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction a) →
                (Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f' →
                    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f' →
                      (∀ a ∈ restPrf, Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction a) →
                        Std.Tactic.BVDecide.LRAT.Internal.lratChecker f' restPrf =
                            Std.Tactic.BVDecide.LRAT.Internal.Result.success →
                          Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f') →
                  Std.Tactic.BVDecide.LRAT.Internal.lratChecker f' restPrf =
                      Std.Tactic.BVDecide.LRAT.Internal.Result.success →
                    Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f