1      let ReaderT = ./Type
2  
3  in    λ(r : Type)
4      → λ(m : Type → Type)
5      → λ(a : Type)
6      → λ(f : r → r)
7      → λ(reader : ReaderT r m a)
8      → λ(env : r)
9      → reader (f env)