rw [ofArray_fold_fn_preserves_assignments_size acc cOpt, ih]
n : Nat
arr : Array (Option (DefaultClause n))
hb : (mkArray n unassigned).size = n
acc : Array Assignment
ih : acc.size = n
cOpt : Option (DefaultClause n)
_cOpt_in_arr : cOpt ∈ arr.data
⊢ (ofArray_fold_fn acc cOpt).size = n
no goals