no goals
α : Type u_1
β : Type ?u.42454
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ inits [] = reverse (map reverse (tails (reverse [])))
simp
no goals
α : Type u_1
β : Type ?u.42454
l✝ l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
l : List α
⊢ inits (a :: l) = reverse (map reverse (tails (reverse (a :: l))))
simp [inits_eq_tails l, map_eq_map_iff, reverse_map]