a : Nat
⊢ id a = a