Actual proofs will end up using own and inv, and none of the notions defined in ownership.v
Attach a file by drag & drop or click to upload
Ralf Jung authored