Archived tweet #10590 from the @leastfixedpoint Twitter Archive

@jcreed @BowToChris @maxsnew Huh, maybe it's that on the RHS one P is in negative position, the other positive. So one kind of has to take on the value/proof from the other. Assuming some kind of parametricity like setup.