Skip to content

bupd, fupd: add idempotence lemmas

Ralf Jung requested to merge ralf/upd-idemp into master

I just noticed that for some reason we are missing these lemmas for the update modalities (we have them for □ and similar modalities).

Merge request reports