notation "\complexes" non associative with precedence 90 for @{'C}.
notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
+
+notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
+notation > "x ⊩_term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation > "⊩ " with precedence 60 for @{'Vdash ?}.
+notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
+