rw [ih]
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
hd : α
tl : List α
ih : ∀ (init : γ), foldl f init (tl ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tl
init : γ
⊢ foldl f (foldl f init (map (fun b => (hd, b)) L2)) (tl ×ˢ L2) =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (hd, b)) init L2) tl
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
hd : α
tl : List α
ih : ∀ (init : γ), foldl f init (tl ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tl
init : γ
⊢ foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl f init (map (fun b => (hd, b)) L2)) tl =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (hd, b)) init L2) tl