> let x = ((\x.x) (\x.x)) in (x 5) > > Since A != {} and M1 is an application... That's what I thought originally but I guess it depends on whether you do the Beta reduction before *or* after the assignment to x.