Fix some proofs in examples/fun-op-sem

These appear not to have been updated for the changes to the
simplification tactic shortcuts.

update fun-op-sem example