type s < t
vars x : s; y : t
. def \ f : s -> s . def f x
. def (y as s);
types
s : Type;
t : Type
type
s < t
vars
x : s;
y : t
forall x : s . def \ f : s -> s . def f x
forall y : t . def (y as s)
2.7: ### Hint: not a class 's'
2.14: ### Hint: not a class 't'