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