add proofmode instances for le_upd
We have proofmode instances for le_upd_if because we use them to define our fupd. In Perennial we have our own fupd which I want to define using le_upd, so I'd like to have instances for that, too.
We have proofmode instances for le_upd_if because we use them to define our fupd. In Perennial we have our own fupd which I want to define using le_upd, so I'd like to have instances for that, too.