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

State before:
α : Type
xs : List α
⊢ reverseAccu [] xs = reverse xs
Tactic:
simp [reverseAccu_Eq_reverse_append]
State after:
no goals