diff --git a/algebra/cmra.v b/algebra/cmra.v
index 87f4f717be9238d500ee282647a6362102e6d33d..3fa2eb41759ca5856e19802c49e557ed4fec5378 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -8,6 +8,11 @@ Instance: Params (@op) 2.
 Infix "â‹…" := op (at level 50, left associativity) : C_scope.
 Notation "(â‹…)" := op (only parsing) : C_scope.
 
+(* The inclusion quantifies over [A], not [option A].  This means we do not get
+   reflexivity.  However, if we used [option A], the following would no longer
+   hold:
+     x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2
+*)
 Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
 Infix "≼" := included (at level 70) : C_scope.
 Notation "(≼)" := included (only parsing) : C_scope.
diff --git a/algebra/updates.v b/algebra/updates.v
index 46dcfe7ab38a4786700c2e2e2aacdd697b672783..6b59571200f6e5a229694655593061eae30feaa3 100644
--- a/algebra/updates.v
+++ b/algebra/updates.v
@@ -10,6 +10,10 @@ Notation "x ~l~> y @ mz" := (local_update mz x y) (at level 70).
 Instance: Params (@local_update) 1.
 
 (** * Frame preserving updates *)
+(* This quantifies over [option A] for the frame.  That is necessary to
+   make the following hold:
+     x ~~> P → Some c ~~> Some P
+*)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n mz,
   ✓{n} (x ⋅? mz) → ∃ y, P y ∧ ✓{n} (y ⋅? mz).
 Instance: Params (@cmra_updateP) 1.