have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n
n : Nat
arr : Array (Option (DefaultClause n))
hb : (mkArray n unassigned).size = n
⊢ (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n