Use `binder` in notations for big ops
This means one can write things such as [∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝.
This has been made possible by https://github.com/coq/coq/pull/13265 (since Coq 8.13).
This means one can write things such as [∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝.
This has been made possible by https://github.com/coq/coq/pull/13265 (since Coq 8.13).