Add the zero-width spaces at the *end* of the lines, and a newline before the first context

Pros:
* It does not matter how editors render the 0-width space, everything is always aligned
* In ProofGeneral, there is no more incorrectn indentation of the first line

Cons:
* There is an empty line between the bar ending the Coq context, and the first Iris hypothesis

proofmode/notation.v

@@ -9,19 +9,19 @@ Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
 Notation "​" := Enil (format "​") : proof_scope.
 Notation "Γ ​ H : P" := (Esnoc Γ H P)
   (at level 1, P at level 200,
-   left associativity, format "Γ ​ H  :  P '//'") : proof_scope.
+   left associativity, format "Γ ​ '//' H  :  P") : proof_scope.
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ★ Q" :=
   (of_envs (Envs Γ Δ) ⊢ Q%I)
   (at level 1, Q at level 200, left associativity,
-  format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ★ '//' Q '//'") :
+  format "Γ '//' '--------------------------------------' □ Δ '//' '--------------------------------------' ★ '//' Q '//'") :
   C_scope.
 Notation "Δ '--------------------------------------' ★ Q" :=
   (of_envs (Envs Enil Δ) ⊢ Q%I)
   (at level 1, Q at level 200, left associativity,
-  format "Δ '--------------------------------------' ★ '//' Q '//'") : C_scope.
+  format "Δ '//' '--------------------------------------' ★ '//' Q '//'") : C_scope.
 Notation "Γ '--------------------------------------' □ Q" :=
   (of_envs (Envs Γ Enil) ⊢ Q%I)
   (at level 1, Q at level 200, left associativity,
-  format "Γ '--------------------------------------' □ '//' Q '//'")  : C_scope.
+  format "Γ '//' '--------------------------------------' □ '//' Q '//'")  : C_scope.
 Notation "​​ Q" := (of_envs (Envs Enil Enil) ⊢ Q%I)
   (at level 1, format "​​ Q") : C_scope.