-- load into ghci

"λa: (Type[0] → (Type[0] → Type[0])).\
 λb: (Type[0] → Type[0]). λc: Type[0].\
   ((a c)(b c))"