Fail Definition plus1_plus1 : Type@{Set+1} := Type@{Set+1}.