Proof mode goals in empty context cannot be distinguished from Coq goals
@jung noted this problem somewhere in lambdarust, see below for a simple example:
From iris Require Import proofmode.tactics. Goal forall M (P : uPred M), P ⊣⊢ P. Proof. intros; iSplit. (* Goals look like `P → P` *)
We could add some special symbol to the proof mode notation with the empty context? Any suggestions?