type s

op a : s

op __=[s]__ : forall a . a * a -> Unit

. (op __=[s]__[s] : forall a . a * a -> Unit)(a, a)