intro h
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
⊢ false = true → ∃ i, f.assignments[i.val] = both
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.rupUnits, f.assignments, false) c.negate).2.snd = true
h : false = true
⊢ ∃ i, f.assignments[i.val] = both