simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
⊢ p ⊨ f.insert c
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
⊢ ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x