'norm_hyp' does not normalize hypotheses with 'exists!'

[Atalay-Ileri]

I have a hypothesis in the form of
H: (F * (exists! v h o', [o = Handle h :: o'] * [s h = None] * a |-> v)) d
When I call norm_hyp H i am getting following error message:

Error:
In nested Ltac calls to "norm_hyp", "norm_reified_hyp" and
"rewrite Norm.interpret_l_sort in H", last call failed.
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:

[tchajed]

Hmm this is actually some work, since I don't reify exists at all (though it's obviously useful). I'll solve this properly at some point. In the meantime I'll prove some theorems to do this manipulation manually.