Actual proofs will end up using own and inv, and none of the notions defined in ownership.v