Definition id (T:Type) := Eval vm_compute in T.