intro performRupCheck_success p pf
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
⊢ ((f.insertRatUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true → limplies (PosFin n) f (f.insert c)
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success : ((f.insertRatUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c