apply Exists.intro hsize
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)
acc : Array Assignment
ih : modified_assignments_invariant acc
cOpt : Option (DefaultClause n)
cOpt_in_arr : cOpt ∈ arr.data
hsize : (ofArray_fold_fn acc cOpt).size = n
⊢ modified_assignments_invariant (ofArray_fold_fn acc cOpt)
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)
acc : Array Assignment
ih : modified_assignments_invariant acc
cOpt : Option (DefaultClause n)
cOpt_in_arr : cOpt ∈ arr.data
hsize : (ofArray_fold_fn acc cOpt).size = n
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray_fold_fn acc cOpt)[i.val] = true → unit (i, b) ∈ (ofArray arr).toList