Theorem: LoVe.List.elems_mirror_counterexample (LoVe/Labs/Lab7.lean)

State before:
⊢ ∃ t, elems t ≠ elems (mirror t)
Tactic:
apply Exists.intro badTree
State after:
⊢ elems badTree ≠ elems (mirror badTree)

State before:
⊢ elems badTree ≠ elems (mirror badTree)
Tactic:
simp [List.elems]
State after:
⊢ ¬elems badTree = elems (mirror badTree)