Properties, datums, collateral

[polinavino]

• match the collaterals-non-empty check in Ensure we always have a collateral input. #2302
• combine optional datums (remove from aux data) with the required ones (and add this structure to the integrity hash computation)
• prove some properties in the properties section, add the existing proofs in it's in
  https://github.com/input-output-hk/cardano-ledger-specs/tree/andre/alonzo-spec-properties

Question:
Of the properties left to prove in the list at the bottom of properties.tex, what ones should I prove, and what ones are redundant/weird/non-formalizable/ok to remove?

[JaredCorduan]

looks good to me!