Originally suggested by Gregory Malecha (a while ago), and recently discussed with @haidang.
Quantifiers in atomic triples make perfect sense, but AUs and AAUUs are more confusing when used directly: there, ∃ actually means ∀, and viceversa.
In this proposal, <<< ∀ x, P x >>> e <<< ∃ y, Q x y, RET f x y >>> expands to ∀ Φ, AU << ∃ x, P x >> ... << ∀ y, Q x y COMM Φ (f x y) >> -* WP e {{ Φ }}; then the quantifiers in AUs match the definition and convey the right intuition.
One might fear this is inconsistent. But expanding triples moves quantifiers to the left of a wand, so flipping their polarity follows the tradition from (dependent) currying: (∀ x, P x -∗ Q) ⊣⊢ ((∃ x, P x) -∗ Q).
(Tested locally with dune and Coq 8.13.2).
FWIW, @swasey and @haidang also brought up arguments about caller/callee views, and about the TaDa logic. However, this MR preserves the notation for atomic triples (which agrees with TaDa), and TaDa rules seem to have similar quantifier flipping from a very superficial look (but no, I don't understand everything in flight). Finally, existentials are existentials both at introduction and elimination time; I think the only polarity flip is the one above — atomic triples use AUs in negative position.
