bupd, fupd: add idempotence lemmas

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