α : Type uu
β : Type vv
l₁ l₂ : List α
a : α
l : List α
⊢ reverse l ++ [a] ~ a :: l
α : Type uu
β : Type vv
l₁ l₂ : List α
a : α
l : List α
⊢ reverse (a :: l) ~ a :: l
rw [reverse_cons]
no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
a : α
l : List α
⊢ reverse l ++ [a] ~ a :: l
exact (perm_append_singleton _ _).trans ((reverse_perm l).cons a)