Refactor `UTXO-inductive`

[WhatisRT]

Since I'm thinking about it right now, here are some things that should help readability a bit:

• UTXO-inductive should be renamed to UTXO. It's not an induction rule, so this name is just misleading. I think this name comes from a very old version of the Shelley spec where it was indeed an induction principle, and nobody bothered renaming it.
• We have 5 checks in there that quantify over outputs. It might be a good idea to introduce some kind of validOutput predicate and replace all of those lines with ∀[ (_ , txout) ∈ ∣ txoutsʰ ∣ ] validOutput txout. The only check that shouldn't go there is the one about the NetworkId, because of the next item.
• Finally introduce a transactionWellFormed predicate, which checks all the NetworkId checks as well as the txADhash check from UTXOW. For now I think the best place to check this new predicate is as part of UTXOW.