split at h <;>
  [
    exact ih rfl;
    skip;
    skip;
    simp only at 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
h :
  (match res with
    | encounteredBoth => encounteredBoth
    | reducedToEmpty =>
      match assignment[l.fst.val]! with
      | pos => if l.snd = true then reducedToUnit l else reducedToEmpty
      | neg => if (!l.snd) = true then reducedToUnit l else reducedToEmpty
      | both => encounteredBoth
      | unassigned => reducedToUnit l
    | reducedToUnit l' =>
      match assignment[l.fst.val]! with
      | pos => if l.snd = true then reducedToNonunit else reducedToUnit l'
      | neg => if (!l.snd) = true then reducedToNonunit else reducedToUnit l'
      | both => encounteredBoth
      | unassigned => reducedToNonunit
    | reducedToNonunit => reducedToNonunit) =
    encounteredBoth
⊢ unsatisfiable (PosFin n) assignment
case h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
ih : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
h :
  (match assignment[l.fst.val]! with
    | pos => if l.snd = true then reducedToUnit l else reducedToEmpty
    | neg => if (!l.snd) = true then reducedToUnit l else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit l) =
    encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
h :
  (match assignment[l.fst.val]! with
    | pos => if l.snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!l.snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    encounteredBoth
⊢ unsatisfiable (PosFin n) assignment