have f_limplies_fc := insertRup_entails_safe_insert f f_readyForRupAdd c insertRupContradiction p
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
⊢ p ⊨ f ↔ p ⊨ f'
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f ↔ p ⊨ f'