Hi Freek
So I'd much rather like to be warned (and stopped) by the system when I write something possibly ambiguous, and forced to rephrase it in readable notation.You're throwing away the child with the bath water!
I am not sure what is the "child" I just threw off Taygetos, but the "bath water" for me is definitely the sensitivity of semantics to transpositions of the directives in the header.
Yes, the behavior of /\ with respect to "Subset of" is less than perfect, but I'd rather have that, than have nothing like it at all!
I did not write about having "nothing like it at all". Actually you can have "everything like it" (and more) just (e.g.) by some explicit prioritizing inside the article. And it is definitely less fragile and more understandable.
I would hate to have to use different notation to get /\ have a type of the form "Subset of ..."
Even if that means that you have a "nice text" whose semantics you actually can't tell without a serious research? Was that the goal of formalizing mathematics? Subset of what? A or B? If it only can be A, then you'll have it. If it can be both, then you would have to say more. Either globally prioritize one of them, or use a nonambiguous synonym.
Best, Josef