Fix notation issues in #302 and add some missing "operator sections" for (bi)entailment

Fix #302 (closed) (and its new instance in !396 (merged)):

• Add missing spaces when declaring notations. This enables spaces within certain sections, as requested, but that is inconsistent with other notations, so should be reconsidered — see my review comment below.
• That leaves an ambiguity for ⊢@{; fix that by adding a notation ( '⊢@{' PROP } Q ) to enable left-factoring (see source-code comment for details).

Also, add new notations (.⊢ Q), (P ⊢.), (P ⊣⊢.), (.⊣⊢ Q), as requested by @robbertkrebbers, and their ASCII variants for consistency. Finally, add a bunch of new testcases with different combinations of spaces as requested.