[Dijkstra] UTXO: Check that tx inputs exist both in the original utxo and the evolving utxo

[carlostome]

The CIP specifies that:

All inputs of all transactions in a single batch must be contained in the UTxO set before any of the
batch transactions are applied. This ensures that operation of scripts is not disrupted, for example, by
temporarily duplicating thread tokens, or falsifying access to assets via flash loans.
In the future, this may be up for reconsideration.

The check in UTXO:

formal-ledger-specifications/src/Ledger/Dijkstra/Specification/Utxo.lagda.md

Line 125 in f1b59f7

∙ SpendInputsOf tx ⊆ dom (UTxOOf Γ) -- (1)

alone addresses this but is insufficient. A previously applied (sub)tx might have spent the input.
It is necessary to check that the input to be spent is part of the evolving UTxO.