no goals
α : Type u_1
β : Type ?u.309365
γ : Type ?u.309368
σ : Type ?u.309371
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l₁ l₂ : List α
⊢ List.foldr (fun b s => ((l₁, l₂), b, s).snd.fst :: ((l₁, l₂), b, s).snd.snd) (l₁, l₂).snd (l₁, l₂).fst = l₁ ++ l₂
induction l₁ <;> simp [*]