exact List.foldlRecOn arr.data ofArray_fold_fn (mkArray n unassigned) hb hl
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
no goals