Hi, Shin-Cheng Mu wrote:

exp2 = \m::N -> \n::N -> \f::(b -> b) -> \b::b -> n [b->b] (m[b]) f b

Oops.. it should be exp2 = \m::N -> \n::N -> \f::(b -> b) -> \b::b -> n [b] (m[b]) f b sincerely, Shin-Cheng Mu