The current axioms of BI imply emp ≡ True

As the subject states, the current axiomatization of the plainly modality implies emp ≡ True. In particular, the guilty parties are the axioms prop_ext and plainly_emp_intro.

I am not sure whose axioms they are, but I hope either @robbertkrebbers or @jjourdan knows the history.

I believe this must be an error, since otherwise there is no point in having emp.

From iris.bi Require Import interface.

Import bi.

Section bi_emp.
Context {PROP : bi}.

Notation "P ⊢ Q" := (@bi_entails PROP P%I Q%I).

Lemma bar: emp ⊢ (True → emp) ∧ (emp → True).
Proof.
  apply and_intro.
  - apply impl_intro_r, and_elim_l.
  - apply impl_intro_r, pure_intro; exact I. 
Qed.

Lemma baz: True ⊢ ((True : PROP) ≡ emp).
Proof.
  transitivity (bi_plainly (emp : PROP))%I; first apply plainly_emp_intro.
  transitivity (bi_plainly ((True → emp : PROP) ∧ (emp → True))%I).
  { apply plainly_mono, bar. }
  apply prop_ext.
Qed.    

End bi_emp.