idris-0.9.9: test/reg001/reg001.idr

apply : (a -> b) -> a -> b
apply f x = f x

class Functor f => VerifiedFunctor (f : Type -> Type) where 
   identity : (fa : f a) -> map id fa = fa 

data Imp : Type where 
   MkImp : {any : Type} -> any -> Imp

testVal : Imp
testVal = MkImp (apply id Z)