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

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