Inference rule with two conclusions or rather inverse function application
Let us introduce an auxiliary predicate $t \downarrow$ whose intended meaning is "$t$ evaluates to something". Its inference rule is
$$\frac{t \Downarrow v}{t \downarrow}.$$
Now you can express your condition with the following two rules:


If $\Delta(t)$ evaluates to $v$ and $t$ evaluates $v'$ then $v$ equals $\Delta(v')$:
$$\frac{\Delta(t) \Downarrow v \qquad t \Downarrow v'}{\Delta(v') = v}$$
If $\Delta(t)$ evaluates to something then so does $t$:
$$\frac{\Delta(t) \downarrow}{t \downarrow}$$.


This is not quite the same as using first-order logic and writing $(\exists v . \Delta(t) \Downarrow v) \implies \exists v' . t \Downarrow v'$. You have to go "meta" and use inversion to conclude from $t \downarrow$ that there exists $v'$ such that $t \Downarrow v'$.

By the way, you said that "since the implication operator $\Rightarrow$ is already used in my dynamic semantics, I'd rather use an inference rule to express the implication" That's a pretty awful reason to choose inference rules over axioms (which is what an implication would give you). You should ask instead what your semantics is for. If you are interested in operational semantics, i.e., you want to express how your programs will be executed, then the rule you are talking about does not really contribute anything. If you want your semantics for reasoning about $\Delta$ and $\Downarrow$, then it might actually be use good old first-order logic.