a9ac4d0904b5547e612f9a394b24666c1ea02ccbChristian Maedervar a : +Type

a9ac4d0904b5547e612f9a394b24666c1ea02ccbChristian Maedertype p a := Pred (Pred a) %% should be correct

a9ac4d0904b5547e612f9a394b24666c1ea02ccbChristian Maedertype p a := Pred a %% should be wrong

a9ac4d0904b5547e612f9a394b24666c1ea02ccbChristian Maedertype m (b : -Type) := b %%

a9ac4d0904b5547e612f9a394b24666c1ea02ccbChristian Maedertype m (b : +Type) := b %% both contradict