add another ▷ paradox by Yusuke

This one is actually a lot simpler than the one based on saved propositions. :)

This is nice. Perhaps we could use nested sections so that it is clear that we use exactly the same axioms for fupd and inv and the STS. (This also avoids all the proof mode instances for fupd that are now copy/pasted.)

Talking about the latter: there is actually a subtle difference. The original paradox only needs finished γ to be duplicable and the new one (in this MR) needs it to be persistent. Do you really need the latter, or is that just for convenience?

As far as I can tell, persistence is required.

Perhaps we could use nested sections so that it is clear that we use exactly the same axioms for fupd and inv and the STS. (This also avoids all the proof mode instances for fupd that are now copy/pasted.)

One cannot put a module into a section, so if we do this we'll have to rename the identifiers in those sections to avoid any conflicts.

added 1 commit

• a7913501 - add another ▷ paradox by Yusuke

Compare with previous version

added 1 commit

• 739b1be3 - share the invariant assumptions between the two inv paradoxes

Compare with previous version

resolved all threads

Modulo nit this looks good to me!

added 1 commit

• 9901fd9c - indentation

Compare with previous version

resolved all threads

enabled an automatic merge when the pipeline for 9901fd9c succeeds

merged

mentioned in commit 6839ae86