intro h
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
res : ReduceResult (PosFin n)
ih : res = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
⊢ reduce_fold_fn assignment res l = encounteredBoth → unsatisfiable (PosFin n) assignment
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
res : ReduceResult (PosFin n)
ih : res = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
h : reduce_fold_fn assignment res l = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment