simp only [insertUnit]
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
b : Bool
l : Literal (PosFin n)
⊢ (insertUnit (units, assignments, b) l).snd.fst.size = assignments.size
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
b : Bool
l : Literal (PosFin n)
⊢ (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, b)
          else
            (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
              b || assignments[l.fst.val]! != unassigned)).snd.fst.size =
    assignments.size