delta : a : Type -> (b : Type -> b -> b) -> a -> a.
[] delta --> a : Type => x : (Type -> Type) => x (a -> a) (x a).