simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x