type s

op a : s

var a : Type

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

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

. a =[s] a

. a =e=[a] a