intro hc p pf
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
performRatCheck_success : (f.performRatCheck negPivot ratHint).snd = true
c : DefaultClause n
⊢ f.clauses[ratHint.fst]! = some c → limplies (PosFin n) f (c.delete negPivot)
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
performRatCheck_success : (f.performRatCheck negPivot ratHint).snd = true
c : DefaultClause n
hc : f.clauses[ratHint.fst]! = some c
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ c.delete negPivot