α : Type u_1
β : Type ?u.315388
γ : Type ?u.315391
σ : Type ?u.315394
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List α
⊢ List.foldr (fun b s => Nat.succ s) 0 l = List.length l
α : Type u_1
β : Type ?u.315388
γ : Type ?u.315391
σ : Type ?u.315394
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List α
⊢ List.foldr (fun b s => (fun a b => Nat.succ (a, b).snd.snd) (l, b, s).fst (l, b, s).snd) 0 (id l) = List.length l
dsimp
no goals
α : Type u_1
β : Type ?u.315388
γ : Type ?u.315391
σ : Type ?u.315394
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
l : List α
⊢ List.foldr (fun b s => Nat.succ s) 0 l = List.length l
induction l <;> simp [*]