List fold lemmas for runtime-approximation proofs

These two list-generic lemmas align the flat and nested index traversals used by convolution and linear-algebra error bounds.

theorem Proofs.RuntimeApprox.NFBackend.foldl_congr {α β : Type} (l : List β) (f g : α → β → α) (init : α) (h : ∀ (a : α) (b : β), f a b = g a b) : List.foldl f init l = List.foldl g init l

Replace the step function of a left fold by a pointwise equal function.

theorem Proofs.RuntimeApprox.NFBackend.foldl_flatMap {α β γ : Type} (l : List α) (g : α → List β) (f : γ → β → γ) (init : γ) : List.foldl f init (List.flatMap g l) = List.foldl (fun (acc : γ) (a : α) => List.foldl f acc (g a)) init l

A fold over flatMap agrees with the corresponding nested fold.