∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (arr : Array (Option β)),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.ofArray arr)