refine ⟨f_readyForRupAdd.1, f_readyForRupAdd.2.1, ?_⟩
case h_1
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
heq✝ : c.isUnit = none
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments }.readyForRupAdd
case h_1
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
heq✝ : c.isUnit = none
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                assignments := f.assignments }.assignments[i.val] =
        true →
      unit (i, b) ∈
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }.toList