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

State before:
α : Type
xs : List α
⊢ reverseAccu [] (reverseAccu [] xs) = xs
Tactic:
simp [reverseAccu_eq_reverse, reverse_reverse]
State after:
no goals