@{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
}.
+notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'exists2 (λ${ident x0}.$P0) (λ${ident x0}.$P1) }.
+
+notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'exists2 (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) }.
+
(* sigma ********************************************************************)
notation < "hvbox(\Sigma ident i : ty break . p)"
notation > "hvbox({ ident i | term 19 p })" with precedence 90
for @{ 'subset (\lambda ${ident i}. $p)}.
-notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+notation < "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
-notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+notation > "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
notation "hvbox(a break ∈ b)" non associative with precedence 45
for @{ 'mem $a $b }.
+notation "hvbox(a break ∉ b)" non associative with precedence 45
+for @{ 'notmem $a $b }.
+
notation "hvbox(a break ≬ b)" non associative with precedence 45
for @{ 'overlaps $a $b }. (* \between *)
notation < "maction (mstyle color #ff0000 (…)) (t)"
non associative with precedence 90 for @{'hide $t}.
-
-notation "⊤" non associative with precedence 90 for @{'true}.
-notation "⊥" non associative with precedence 90 for @{'false}.