-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.mk : {α : outParam (Type u)} →
  {β : outParam (Type v)} →
    [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] →
      {σ : Type w} →
        [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] →
          (toList : σ → List β) →
            (ReadyForRupAdd ReadyForRatAdd : σ → Prop) →
              (ofArray : Array (Option β) → σ) →
                (∀ (arr : Array (Option β)), ReadyForRupAdd (ofArray arr)) →
                  (∀ (arr : Array (Option β)), ReadyForRatAdd (ofArray arr)) →
                    (insert : σ → β → σ) →
                      (∀ (f : σ) (c1 c2 : β), c2 ∈ toList (insert f c1) ↔ c2 = c1 ∨ c2 ∈ toList f) →
                        (∀ (f : σ) (c : β), ReadyForRupAdd f → ReadyForRupAdd (insert f c)) →
                          (∀ (f : σ) (c : β), ReadyForRatAdd f → ReadyForRatAdd (insert f c)) →
                            (delete : σ → Array ℕ → σ) →
                              (∀ (f : σ) (arr : Array ℕ), ∀ c ∈ toList (delete f arr), c ∈ toList f) →
                                (∀ (f : σ) (arr : Array ℕ), ReadyForRupAdd f → ReadyForRupAdd (delete f arr)) →
                                  (∀ (f : σ) (arr : Array ℕ), ReadyForRatAdd f → ReadyForRatAdd (delete f arr)) →
                                    (∀ (p : α → Bool) (f : σ),
                                        Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f =
                                          (((toList f).all fun c =>
                                              decide (Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c)) =
                                            true)) →
                                      (performRupAdd : σ → β → Array ℕ → σ × Bool) →
                                        (∀ (f : σ) (c : β) (rupHints : Array ℕ) (f' : σ),
                                            ReadyForRupAdd f →
                                              performRupAdd f c rupHints = (f', true) → f' = insert f c) →
                                          (∀ (f : σ) (c : β) (rupHints : Array ℕ) (f' : σ),
                                              ReadyForRupAdd f →
                                                performRupAdd f c rupHints = (f', true) →
                                                  Std.Tactic.BVDecide.LRAT.Internal.Liff α f f') →
                                            (performRatAdd :
                                                σ → β → Std.Sat.Literal α → Array ℕ → Array (ℕ × Array ℕ) → σ × Bool) →
                                              (∀ (f : σ) (c : β) (p : Std.Sat.Literal α) (rupHints : Array ℕ)
                                                  (ratHints : Array (ℕ × Array ℕ)) (f' : σ),
                                                  ReadyForRatAdd f →
                                                    p ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c →
                                                      performRatAdd f c p rupHints ratHints = (f', true) →
                                                        f' = insert f c) →
                                                (∀ (f : σ) (c : β) (p : Std.Sat.Literal α) (rupHints : Array ℕ)
                                                    (ratHints : Array (ℕ × Array ℕ)) (f' : σ),
                                                    ReadyForRatAdd f →
                                                      p ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c →
                                                        performRatAdd f c p rupHints ratHints = (f', true) →
                                                          Std.Tactic.BVDecide.LRAT.Internal.Equisat α f f') →
                                                  Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ