module apply_function where

postulate A : Set 
postulate f : {B : Set} -> A -> B

->E : {B : Set} -> A -> (A -> B) -> B
->E a f = f a