`BookProof.BrstReducedTransfer.exactStates_le_physicalStates` (hnil : ∀ x, Om (Om x) = 0) : exactStates Om ≤ physicalStates Om

Initializing...

`BookProof.BrstReducedTransfer.exactStates_le_physicalStates` (hnil : ∀ x, Om (Om x) = 0) : exactStates Om ≤ physicalStates Om · Prove2Me