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".
