simp only [ofArray, Array.foldl_eq_foldl_data]
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).assignments.size = n
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n