exact List.foldlRecOn l f assignments hb hl
α : Type u
assignments : Array Assignment
f : Array Assignment → α → Array Assignment
f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size
l : List α
hb : assignments.size = assignments.size
hl :
  ∀ (assignments' : Array Assignment),
    assignments'.size = assignments.size → ∀ (a : α), a ∈ l → (f assignments' a).size = assignments.size
⊢ (List.foldl f assignments l).size = assignments.size
no goals