diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 0bbd38a5ea1583626d83949376bc03e025a6e474..1f9e4859c32cad0ccc5de5cacd6e293e14f32e02 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -4,7 +4,7 @@ Import uPred.
 
 (** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
 [Σ]. This class is similar to the [subG] class, but written down in terms of
-individual CMRAs instead of lists of CMRA functors. This additional class is
+individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
 needed because Coq is otherwise unable to solve type class constraints due to
 higher-order unification problems. *)
 Class inG (Σ : gFunctors) (A : cmraT) :=
diff --git a/program_logic/model.v b/program_logic/model.v
index 789c57a5beddd20183283ec8795cedd263767bce..117809723654822129b0c2412aad243823dd6b1e 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -101,7 +101,7 @@ Proof.
   move=> H i; move: H=> /(_ i) [j ?].
   exists (Fin.L _ j). by rewrite /= fin_plus_inv_L.
 Qed.
-Instance inGF_app_r Σ Σ1 Σ2 : subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
+Instance subG_app_r Σ Σ1 Σ2 : subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
 Proof.
   move=> H i; move: H=> /(_ i) [j ?].
   exists (Fin.R _ j). by rewrite /= fin_plus_inv_R.