solve_ndisj doesn't work for goals of the form `∅ ## ↑N`
However, set_solver
works in this case.
Minimal example:
From stdpp Require Import namespaces coPset.
Goal (∅ : coPset) ## ↑(nroot.@0).
Proof. set_solver. (* solve_ndisj does not work *) Qed.
Goal (↑(nroot.@1) : coPset) ## ↑(nroot.@0).
Proof. solve_ndisj. (* set_solver. does not work *) Qed.
Edited by Dan Frumin