Definition toto (x : Set) := x.

(* <Warning> : Grammar is replaced by Notation *)