have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.data) :
  (ofArray_fold_fn acc cOpt).size = n := by rw [ofArray_fold_fn_preserves_assignments_size acc cOpt, ih]
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
n : Nat
arr : Array (Option (DefaultClause n))
hb : (mkArray n unassigned).size = n
hl :
  ∀ (acc : Array Assignment),
    acc.size = n → ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.data → (ofArray_fold_fn acc cOpt).size = n
⊢ (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.data).size = n