idris-1.0: samples/tutorial/Universe.idr

myid : (a : Type) -> a -> a
myid _ x = x

idid :  (a : Type) -> a -> a
idid = myid _ myid