diff --git a/iris/bi/internal_eq.v b/iris/bi/internal_eq.v
index 6dd1a42a78b717e431691b4e8228639d903dcaec..0cf55bb45d6978697f4d6e4337cd0766734887f4 100644
--- a/iris/bi/internal_eq.v
+++ b/iris/bi/internal_eq.v
@@ -6,7 +6,7 @@ Import interface.bi derived_laws.bi derived_laws_later.bi.
 Internal equality is not part of the [bi] canonical structure as [internal_eq]
 can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
 [▷ (x ≡ y) ⊢ Next x ≡ Next y] if the BI is step-indexed. *)
-Class InternalEq (PROP : bi) :=
+Class InternalEq (PROP : Type) :=
   internal_eq : ∀ {A : ofe}, A → A → PROP.
 Global Arguments internal_eq {_ _ _} _ _ : simpl never.
 Global Hint Mode InternalEq ! : typeclass_instances.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 81c8c326b9ea1b8f1ae4db6c3cc3e0ae3f590adb..4109333d983075175ba8c56cfd1ec740238b73f9 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -6,15 +6,15 @@ Import interface.bi derived_laws.bi derived_laws_later.bi.
 (* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 
-Class Plainly (A : Type) := plainly : A → A.
-Global Arguments plainly {A}%type_scope {_} _%I.
+Class Plainly (PROP : Type) := plainly : PROP → PROP.
+Global Arguments plainly {PROP}%type_scope {_} _%I.
 Global Hint Mode Plainly ! : typeclass_instances.
 Global Instance: Params (@plainly) 2 := {}.
 Notation "â–  P" := (plainly P) : bi_scope.
 
 (* Mixins allow us to create instances easily without having to use Program *)
 Record BiPlainlyMixin (PROP : bi) `(Plainly PROP) := {
-  bi_plainly_mixin_plainly_ne : NonExpansive (plainly (A:=PROP));
+  bi_plainly_mixin_plainly_ne : NonExpansive (plainly (PROP:=PROP));
 
   bi_plainly_mixin_plainly_mono (P Q : PROP) : (P ⊢ Q) → ■ P ⊢ ■ Q;
   bi_plainly_mixin_plainly_elim_persistently (P : PROP) : ■ P ⊢ <pers> P;