simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq] at pf
case inr
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
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
⊢ p ⊨ c'