rw [ofArray_fold_fn]
n : Nat
assignments : Array Assignment
cOpt : Option (DefaultClause n)
⊢ (ofArray_fold_fn assignments cOpt).size = assignments.size
n : Nat
assignments : Array Assignment
cOpt : Option (DefaultClause n)
⊢ (match cOpt with
      | none => assignments
      | some c =>
        match c.isUnit with
        | none => assignments
        | some (l, true) => assignments.modify l.val addPosAssignment
        | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size