Theorem: LRAT.DefaultFormula.insertRupUnits_preserves_clauses (LeanSAT/LRAT/Formula/RupAddResult.lean)

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (f.insertRupUnits units).fst.clauses = f.clauses
Tactic:
rw [insertRupUnits]
State after:
no goals