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

State before:
x y z : ℕ
hxy : x = y
hyz : y = z
⊢ x = z
Tactic:
prove_direct
State after:
no goals