[Alonzo] collectP2ScriptWithContext should not drop scripts

`collectP2ScriptWithContext` is collecting scripts to validate a transaction.

For each script, the function needs to do a few lookups that are assumed to succeed, but if they fail, the scripts are omitted from the result, with the consequence that they will be ignored when validating the transaction.

To ensure that the lookups succeed, there are separate premises in the UTXOW rule. It happened that some of these premises were missing in the Agda specification [[link]](https://github.com/IntersectMBO/formal-ledger-specifications/pull/1035#issuecomment-3773628055). To help catch these omissions, we could attempt to prove that the premises in the UTXOW rule suffice to prove that the length of the returned list is equal to the amount of scripts needed by the transaction.