Theorem: LoVe.List.reverse_twice (LoVe/Lectures/LoVe08_Metaprogramming_Demo.lean)

State before:
xs : List ℕ
⊢ List.reverse (List.reverse xs) = xs
Tactic:
prove_direct
State after:
no goals