postulate A:: Set

f  :: ((A -> A)-> A) -> A
   = \(aaa::(A -> A)-> A)-> 
       let aa::A -> A
             = \(a::A)-> 
               a
       in  aaa aa


postulate John_is_a_student :: Set

postulate Human_Beings:: Set

postulate John :: Human_Beings

postulate Mary :: Human_Beings

postulate is_Student:: Human_Begins -> Set

postulate p :: is_Student John

postulate q :: is_Student John -> is_Student Mary