TSL question: function constraints

[w14]

A small question about TSL semantics. I'm just verifying because I know sometimes tslsynth gives messages that are not exactly correct.

Question

If you assume that a variable equals a function, will the spec be always unrealizable because the spec needs to work for any choice of function? Or will the condition place constraints on f?

In an example, suppose you have a spec in an "always guarantee" block and it produces an output. If you add a condition that a function f must equal y, as shown below, will this simply place constraints on possible fs? Or will it always be unrealizable because the spec needs to work for any possible choice of "f" and so you can't place constraints on f.

always assume {
	f x == X y
}

always guarantee {
	[terms involving f, x, and [y <- ...]]
}