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.