https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/c72bfec9e38531b7dc70f05c2415ed1e3f806899 demonstrates some cases that
solve_ndisj cannot handle, and it'd be great if it could. Most of them could be handled if we added
Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
The one remaining case is more subtle. It is solved by
assert (↑shrN ⊆ (↑lrustN : coPset)) by solve_ndisj. set_solver., but is there a way we can plug solve_ndisj and set_solver together so that we don't have to say in advance which inclusions we need?