Theorem: LoVe.Nat.Eq_symm (LoVe/Lectures/LoVe08_Metaprogramming_Demo.lean)

State before:
x y : ℕ
h : x = y
⊢ y = x
Tactic:
prove_direct
State after:
no goals