Theorem: eq_is_symm (Instructor/Exams/Final/final_part1_key.lean)

State before:
α : Type
a b : α
h : a = b
⊢ b = a
Tactic:
rw [h]
State after:
no goals