+(* exists *******************************************************************)
+
+notation "hvbox(∃ _ break . p)"
+ with precedence 20
+for @{'exists $p }.
+
+notation < "hvbox(\exists ident i : ty break . p)"
+ right associative with precedence 20
+for @{'exists (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\exists ident i break . p)"
+ with precedence 20
+for @{'exists (\lambda ${ident i}. $p) }.
+
+(*