∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n),
  some c ∈ f.clauses.toList →
    (∃ a,
        (a, false) ∈ units ∧ Std.Tactic.BVDecide.LRAT.Internal.Clause.unit (a, false) = c ∨
          (a, true) ∈ units ∧ Std.Tactic.BVDecide.LRAT.Internal.Clause.unit (a, true) = c) ∨
      some c ∈ f.clauses.toList ∨
        (∃ a,
            (a, false) ∈ f.rupUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
              (a, true) ∈ f.rupUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c) ∨
          ∃ a,
            (a, false) ∈ f.ratUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, false) = c ∨
              (a, true) ∈ f.ratUnits.toList ∧ Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit (a, true) = c