solve_ndisj: try harder
In my logically atomic stack, the following goal fails to be solved currently but is solved after this patch:
⊤ ∖ ↑stackN ⊆ ⊤ ∖ ↑offerN ∖ ↑protoN
where
Definition stackN : namespace := nroot .@ "logatom_stack".
Definition offerN : namespace := nroot .@ "logatom_stack" .@ "offer".
Definition protoN : namespace := nroot .@ "logatom_stack" .@ "protocol".
Edited by Ralf Jung