idris-0.9.0: tutorial/examples/universe.idr

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

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