def Id (type : Type u) : Type u

@[always_inline]

instance Id.instMonadId : Monad Id

def Id.hasBind : Bind Id

@[inline]

def Id.run {α : Type u_1} (x : Id α) : α

instance Id.instOfNatId {α : Type u_1} {n : Nat} [OfNat α n] : OfNat (Id α) n