solve_ndisj cannot solve `⊤ ∖ ↑N1 ∖ ↑N2 ⊆ ⊤ ∖ ↑N1.@"x" ∖ ↑N2 ∖ ↑N1.@"y"`

The following fails:

Lemma test5 (N1 N2 : namespace) :
  ⊤ ∖ ↑N1 ∖ ↑N2 ⊆@{coPset} ⊤ ∖ ↑N1.@"x" ∖ ↑N2 ∖ ↑N1.@"y".
Proof. solve_ndisj. Qed.

However, I think this is in the realm of what solve_ndisj should be able to handle, and the lemmas we got for it are indeed enough:

Lemma test5 (N1 N2 : namespace) :
  ⊤ ∖ ↑N1 ∖ ↑N2 ⊆@{coPset} ⊤ ∖ ↑N1.@"x" ∖ ↑N2 ∖ ↑N1.@"y".
Proof.
  apply namespace_subseteq_difference.
  { apply ndot_preserve_disjoint_r. set_solver. }
  solve_ndisj.
Qed.

The problem is related to the ordering of terms, the following goal can be solved:

Lemma test5' (N1 N2 : namespace) :
  ⊤ ∖ ↑N1 ∖ ↑N2 ⊆@{coPset} ⊤ ∖ ↑N1.@"x" ∖ ↑N1.@"y" ∖ ↑N2.

Notice how the N appear in the same order on both sides.

Cc @gparthas who ran into this in practice.

changed the description

mentioned in merge request !75 (merged)

closed via commit 9d08f65f