diff --git a/iris_meta.v b/iris_meta.v
index 47d850365199ef3f353ce26a6a55b88bcef04347..d75aa2f42deb8a5146e714d80a36b30d2a81f834 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -232,6 +232,8 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
     Hypothesis fillE : forall K e, E (K [[e]]) == E e * E (K [[fork_ret]]).
     
     (* One can prove forkE, fillE as valid internal equalities. *)
+    (* RJ: We don't have rules for internal equality of propositions, don't we? Maybe we should have an axiom,
+       saying they are equal iff they are equivalent. *)
     Remark valid_intEq {P P' : Props} (H : valid(P === P')) : P == P'.
     Proof. move=> w n r; exact: H. Qed.