diff --git a/theories/examples/graph/graph.v b/theories/examples/graph/graph.v
index f179212b9a22ffc077786fb5337557b3b1732d2a..8e5ff9c140b5f64a1ce33b4715729577f8ba768e 100644
--- a/theories/examples/graph/graph.v
+++ b/theories/examples/graph/graph.v
@@ -25,13 +25,14 @@ Definition pair_in_set `{Countable A} (Ps : gset (A * A)) (S : gset A) : Prop
 Definition pair_in_bound (Ps : gset (event_id * event_id)) (n : event_id) : Prop
   := set_Forall (λ p, p.1 < n ∧ p.2 < n)%nat Ps.
 
+(* We don't need so ⊆ (po ∪ com)+ because we don't have po. The view inclusion
+  relation includes po, among other relations. *)
 Record graph {A : Type} := mkGraph {
   Es  : event_list A;
   com : gset (event_id * event_id) ;
   so  : gset (event_id * event_id) ;
   gcons_com_included_dec : bool_decide (pair_in_bound com (length Es));
   gcons_so_included_dec  : bool_decide (pair_in_bound so (length Es)) ;
-  (* TODO: so ⊆ (po ∪ com)+ ? *)
 }.
 
 Global Arguments graph : clear implicits.
diff --git a/theories/examples/queue/proof_per_elem_graph.v b/theories/examples/queue/proof_per_elem_graph.v
index 651e05e4c8320167f42dfb0f0c7f835bfaa80913..2bdac0e19f7a3fd2861c22a9ff4f671d6daba6cd 100644
--- a/theories/examples/queue/proof_per_elem_graph.v
+++ b/theories/examples/queue/proof_per_elem_graph.v
@@ -57,6 +57,7 @@ Definition QueuePerElem γg : vProp :=
   ∃ G M, msq.(QueueLocal) (N .@ "que") γg q G M ∗
          inv (N .@ "iinv") (QueuePerElemInv γg).
 
+(* TODO: we can prove logically-atomic spec here. *)
 Lemma per_elem_enqueue (DISJ: N ## histN) γg (x: Z) tid (NZ: 0 < x) :
   {{{ QueuePerElem γg ∗ ▷ P x}}}
       msq.(enqueue) [ #q; #x] @ tid; ⊤