simp only [performRupCheck, Prod.mk.eta] at performRupCheck_success
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRupUnits c.negate).1.clauses)
            ((f.insertRupUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
⊢ p ⊨ f.insert c