α : Type ?u.312965
β : Type ?u.312968
γ : Type ?u.312971
σ : Type ?u.312974
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Nat.rec [] (fun n IH => IH ++ [n]) n = List.range n
α : Type ?u.312965
β : Type ?u.312968
γ : Type ?u.312971
σ : Type ?u.312974
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Nat.rec [] (fun n_1 IH => (n, n_1, IH).snd.snd ++ [(n, n_1, IH).snd.fst]) (id n) = List.range n
simp
no goals
α : Type ?u.312965
β : Type ?u.312968
γ : Type ?u.312971
σ : Type ?u.312974
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
⊢ Nat.rec [] (fun n IH => IH ++ [n]) n = List.range n
induction n <;> simp [*, List.range_succ]