induction L1 generalizing init <;> simp
γ : Type u_1
α : Type u_2
β : Type u_3
L1 : List α
L2 : List β
f : γ → α × β → γ
init : γ
⊢ foldl f init (L1 ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init L1
case cons
γ : Type u_1
α : Type u_2
β : Type u_3
L2 : List β
f : γ → α × β → γ
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (init : γ), foldl f init (tail✝ ×ˢ L2) = foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) init tail✝
init : γ
⊢ foldl f (foldl f init (map (fun b => (head✝, b)) L2)) (tail✝ ×ˢ L2) =
    foldl (fun acc a => foldl (fun acc b => f acc (a, b)) acc L2) (foldl (fun acc b => f acc (head✝, b)) init L2) tail✝