Предположим, я хочу конвертировать ~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. Возможно ли это?