This was done using the following sed script:
sed -i -E 's/Instance ([a-zA-Z0-9_]+)( .*: (Op|P?Core|ValidN?|Unit) )/Instance \1_instance\2/' $(find iris/algebra -name "*.v")
Some manual fixup was needed; see the second commit for that. We might want to do something about some of these proofs?
This rename opens the opportunity of renaming lemmas such as frac_valid'
to remove the '
that makes no sense here.