implement and proof canonicalizeFixedEra
implement and prove eraSeq
a bit of cleanup