rfl
case h_2
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
heq✝ : f.clauses[ratHint.fst]! = none
⊢ ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }, false).fst =
    f
no goals