1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
Implicit Arguments On. Mod M. Definition a:=[s:Set]s. Print a. EndM M. Print M.a. Mod K. Definition app:=[A,B:Set; f:(A->B); x:A](f x). Mod N. Definition apap:=[A,B:Set](app (app 1!A 2!B)). Print app. Print apap. EndM N. Print N.apap. EndM K. Print K.app. Print K.N.apap. Mod W:=K.N. Print W.apap.