Section S.
Let bla@{} := Prop.
Let bli@{u} := Type@{u}.
Fail Let blo@{} := Type.
End S.