. rfl
case h_1
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
⊢ assignments.size = assignments.size

case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (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
case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (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