have hb : modified_assignments_invariant (mkArray n unassigned) := by
  have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
  apply Exists.intro hsize
  intro i b h
  by_cases hb : b <;> simp [hasAssignment, hb, hasPosAssignment, hasNegAssignment] at h
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList