Theorem: LoVe.reverseAccu_Eq_reverse_append (LoVe/Labs/Lab4Solution.lean)

State before:
α : Type
as : List α
⊢ reverseAccu as [] = reverse [] ++ as
Tactic:
rfl
State after:
no goals

State before:
α : Type
as : List α
x : α
xs : List α
⊢ reverseAccu as (x :: xs) = reverse (x :: xs) ++ as
Tactic:
simp [reverse, reverseAccu, reverseAccu_Eq_reverse_append _ xs]
State after:
no goals