Add missing commutations for `fupd`

Merged Paolo G. Giarrusso requested to merge Blaisorblade/iris:fupd-commutes into master

Suggestion from Gregory Malecha, proof scripts from me.

Edited by Paolo G. Giarrusso

Merge request reports