no goals
α : Type u
β : Type v
γ : Type w
as : List α
⊢ length (reverse as) = length as
induction as with
| nil => rfl
| cons a as ih => simp [ih]
no goals
case nil
α : Type u
β : Type v
γ : Type w
⊢ length (reverse nil) = length nil
rfl
no goals
case cons
α : Type u
β : Type v
γ : Type w
a : α
as : List α
ih : length (reverse as) = length as
⊢ length (reverse (a :: as)) = length (a :: as)
simp [ih]