let signature S = theory {
  F :: (x : Nat) (y : Bool) -> Set,
  G :: (z : set-of(F 3 4)) -> Set // this sould fail
}