Refactor `UTXO-inductive`

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`.