case nil
α : Type u_1
β : Type ?u.48588
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ length (tails []) = length [] + 1

case cons
α : Type u_1
β : Type ?u.48588
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
x : α
l : List α
IH : length (tails l) = length l + 1
⊢ length (tails (x :: l)) = length (x :: l) + 1
α : Type u_1
β : Type ?u.48588
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
l : List α
⊢ length (tails l) = length l + 1
induction' l with x l IH
no goals
case nil
α : Type u_1
β : Type ?u.48588
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
⊢ length (tails []) = length [] + 1
simp
no goals
case cons
α : Type u_1
β : Type ?u.48588
l✝ l₁ l₂ l₃ : List α
a b : α
m n : ℕ
x : α
l : List α
IH : length (tails l) = length l + 1
⊢ length (tails (x :: l)) = length (x :: l) + 1
simpa using IH