internal {
type s, t
funs o,q : s -> t
. o = q
}