repeat first
  | rfl
  | simp only [Array.modify_preserves_size]
  | split
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
⊢ (if (b2 || b1) = true then (assignments, derivedLits, b1, b2)
        else
          match clauses[id]? with
          | some (some c) =>
            match c.reduce assignments with
            | ReduceResult.encounteredBoth => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToEmpty => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToUnit (l, b) =>
              if hasAssignment b assignments[l.val]! = true then (assignments, derivedLits, false, false)
              else (assignments.modify l.val (addAssignment b), (l, b) :: derivedLits, false, false)
            | ReduceResult.reducedToNonunit => (assignments, derivedLits, false, true)
          | some none => (assignments, derivedLits, false, true)
          | none => (assignments, derivedLits, false, true)).fst.size =
    assignments.size
no goals