Specifications with dependent existententials cannot be applied
When we make an instance like:
Global Program Instance clone_arc_spec' γ (v : val) :
SPEC ∃ P HP, {{ is_arc P (HP := HP) γ v ∗ token P γ }}
clone v
{{ RET #(); token P γ ∗ token P γ }}.
where HP : Fractional P
, the TC search for FromTExist
fails, so the specification cannot be used.
It works fine if we leave P
as an evar.