- k:b'->σ
- [N]:(a'->σ)->σ
- m:((a'->σ)->σ)->(b'->σ)->σ
- m[N]:(b'->σ)->σ
- m[N]k:σ
- [M]:((a->b)'->σ)->σ = ((((a'->σ)->σ)->(b'->σ)->σ)->σ)->σ
- [M](\m.m[N]k):σ
- [MN]:(b'->σ)->σ