I've only recently started playing with refinement between specs, checking that one spec implies another. For illustrative purposes, we'll say the refinement is `THEOREM B => A`
An early stumbling block I ran into was when I had a `pc` variable that appears in both specs.
B introduces "extra" states, but they only modify variables that don't appear in A. That would normally be fine, except that it causes `pc` to not match.
Is there a right way to more or less ignore a `pc` variable when checking if one spec refines another? I feel like there's a super obvious answer to this, but it's not coming to me.
Thanks,