Theorem: id_eval (FM2023Exrcise/section03_functions/sheet1.lean)

State before:
X Y Z : Type
x : X
⊢ id x = x
Tactic:
rfl
State after:
no goals