Require Export plik.

Definition tutu := [X:Set](toto X).