1  λ(r : Type) → λ(m : Type → Type) → λ(a : Type) → r → m a