I want to express a simple correctness theorem for a term-desugaring function $\Delta$. The goal is to express that if the evaluation of a desugared term yields a value, this value is the desugared result of evaluating the original term. Since the implication operator $\Rightarrow$ is already used in my dynamic semantics, I'd rather use an inference rule to express the implication. However, in the premise I have to introduce a variable $v$ that is the result of applying $\Delta$ to a variable bound in the conclusion. Since there is no inverse of $\Delta$ I am somewhat stuck between two odd variants to express the relation.The first variant uses two conclusions (like multiple premises the idea is that both always hold):$$\frac{\Delta(t) \Downarrow v}{t \Downarrow v^\prime \quad \Delta(v^\prime) = v}$$This looks odd to me. The alternative would be to see the rule as a scheme subject to some substitution over the meta-variables $t$ and $v$. In that case I could also write:$$\frac{\Delta(t) \Downarrow \Delta(v)}{t \Downarrow v}$$This is obviously cleaner, but I am not quite happy with the implications (pun not intended) to the theorem: In the first case, if $v \neq \Delta(v^\prime)$ the premise still holds, but the conclusion does not, so $\Delta$ is not correct. In the second case the premise would not apply - so correctness simply does not cover the case at all. Is there a common pattern to deal with such problems? Did I overlook something?
Inference rule with two conclusions or rather inverse function application
formal languages;programming languages;correctness proof