`BookProof.ChapterStatementOperator.halfUncertain_not_idempotent` (h : ∃ ψ : H, ψ ≠ 0) : ¬ ((halfUncertain (H := H)).op ∘L (halfUncertain (H := H)).op = (halfUncertain (H := H)).op

Initializing...

`BookProof.ChapterStatementOperator.halfUncertain_not_idempotent` (h : ∃ ψ : H, ψ ≠ 0) : ¬ ((halfUncertain (H := H)).op ∘L (halfUncertain (H := H)).op = (halfUncertain (H := H)).op · Prove2Me