> > > 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.
>
> Surely you don't do any reductions (which are equivalent to evaluation)
> before you type it!?
Yes. D'oh!