idris-0.9.6: tutorial/examples/universe.idr

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

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