Theorem: LoVe.reverse_reverse (LoVe/Lectures/LoVe04_ForwardProofs_Demo.lean)

State before:
α : Type
⊢ reverse (reverse []) = []
Tactic:
rfl
State after:
no goals

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