Re: [tlaplus] How can this lemma (involving []) be applied?

[Roy Overbeek <r.over...@xxxxxxxxx>]

Hi Stephan,

Thanks a lot, this is very helpful. In my mental model NEW P and NEW Q approximately meant 'for all (boolean) expressions P and Q', but I now understand the distinctions you've made. It's also nice to see that your proposed proof to the corollary is even shorter than what I had in mind.

Kind regards,

Roy