no goals
α : Type u_1
β : Type ?u.41504
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ tails ([] ++ []) = map (fun l => l ++ []) (tails []) ++ tail (tails [])
simp
no goals
α : Type u_1
β : Type ?u.41504
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
t : List α
⊢ tails ([] ++ a :: t) = map (fun l => l ++ a :: t) (tails []) ++ tail (tails (a :: t))
simp
no goals
α : Type u_1
β : Type ?u.41504
l l₁ l₂ l₃ : List α
a✝ b : α
m n : ℕ
a : α
s t : List α
⊢ tails (a :: s ++ t) = map (fun l => l ++ t) (tails (a :: s)) ++ tail (tails t)
simp [tails_append s t]