Coq: раскрываем хитрые обозначения

Предположим, я хочу преобразовать ~X в X -> False, используя тактику unfold.

У меня есть два варианта, как это сделать: либо по unfold not, либо по unfold "~". Второй способ, по-видимому, более удобен, так как нет необходимости запоминать, какое имя определения стоит за обозначением.

Однако мне не удалось сделать это в более сложных случаях:

Definition assn_sub X a P : Assertion :=
  fun (st : state) =>
    P (X !-> aeval st a ; st).

Notation "P [ X |-> a ]" := (assn_sub X a P)
  (at level 10, X at next level).

и я хочу раскрыть это в выражении

((fun st0 : state => st0 Y = st0 X + st0 Z) [Z |-> Y - X]) st

без использования assn_sub. Является ли это возможным?