have hb : (reducedToEmpty : ReduceResult (PosFin n)) = encounteredBoth → unsatisfiable (PosFin n) assignment := by
  simp only [false_implies]
n : Nat
c : DefaultClause n
assignment : Array Assignment
⊢ c.reduce assignment = encounteredBoth → unsatisfiable (PosFin n) assignment
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
⊢ c.reduce assignment = encounteredBoth → unsatisfiable (PosFin n) assignment