What should delegates with qualifiers mean?

[Timon Gehr]

On 25.03.21 02:01, Timon Gehr wrote:
> Why is removing qualifiers sound? delegate is an existential type:
> 
> B delegate(A)q ≡ ∃C. (A×q(C)*)×q(C)*→B
> 
> ...
x). This is getting a bit embarrassing. Third try:

Why is removing qualifiers sound? delegate is an existential type:

B delegate(A)q ≡ ∃C. (A×q(C)*→B)×q(C)*

Therefore,

B delegate(A)immutable ≡ ∃C. (A×immutable(C)*→B)×immutable(C)* ⊆ ∃C'. 
(A×C'*→B)×C'*,

where we have chosen C' as immutable(C).