let signature S = theory {
    A :: Set,
    Point :: <A>,
    B :: (x : set-of(A)) -> Set
}

let signature T = theory {
    SI :: S,
    F :: (r: set-of((SI .B) (element-of(SI .Point)))) -> Set
}