Re: [tlaplus] Tagged formulas

[Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>]

As (CHOOSE k : k = e)' = (CHOOSE k : k = e') and it must be this way (I don't see how CHOOSE could be any different), that's not what CAPTURE is supposed to do. I want (CAPTURE e)' = (CAPTURE e).