when checking that a specification S1 implements a specification S2 I often
need to augment S1 with a prophecy variable, obtaining S1p.
However I quickly realized that adding prophecy variables is tricky.
I often make mistakes resulting in S1p having less behaviors than S1.
Therefore I would like to check with TLC that all behaviors of S1 are
also behaviors of S1p when the prophecy variable is hidden.
I think that it is not possible to do this with TLC. Am I correct?
Would it be realistic to try to implement a procedure to check formulas of the form S1 => \EE prophecy_var : S1p?