Remark: Ownership is not semantic no-cloning

The type $\mathsf{Q}⊸\mathsf{Q}\otimes \mathsf{Q}$ is inhabited:

has that type. Typing prohibits duplicate ownership, not all terms with a possible cloning type. Universal cloning is excluded semantically in Theorem thm:nocloning. Quantum consumption by an explicit measurement followed by classical deletion is also different from structural quantum weakening.