To make debugging and conformance testing easier, we should limit the main Properties.*agda* file (e.g., src/Ledger/Conway/Specification/Utxo/Properties.lagda) to computational properties and put all others in separate files under the Properties subdirectory (e.g., src/Ledger/Conway/Specification/Utxo/Properties/PoV.lagda.md).