1    λ(f : Type → Type)
2  → λ(g : Type → Type)
3  → λ(a : Type)
4  → ∀(r : Type) → (∀(b : Type) → (f b → a) → g b → r) → r