diff --git a/atomic_sync.v b/atomic_sync.v
index 61236f4d6b5e2d22a8615263cf70d1c09a231f9d..61b3f8d1b6a5c9300cd1a6d7228448fb13fa63cf 100644
--- a/atomic_sync.v
+++ b/atomic_sync.v
@@ -1,11 +1,10 @@
 From iris.program_logic Require Export weakestpre hoare.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import dec_agree frac.
 From iris_atomic Require Import atomic sync misc.
 
-Definition syncR := prodR fracR (dec_agreeR val).
+Definition syncR := prodR fracR (dec_agreeR val). (* track the local knowledge of ghost state *)
 Class syncG Σ := sync_tokG :> inG Σ syncR.
 Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
 
@@ -40,7 +39,7 @@ Section atomic_sync.
                                (∀ (v: val) (g': A),
                                   ϕ l g' -★ β x g g' v ={E}=★ Φ v)
                                ⊢ WP f' x @ E {{ Φ }} )}}.
-  (* XXX (zhen): The linear VS in the above post-condition is for the final step
+  (* The linear view shift in the above post-condition is for the final step
      of computation. The client side of such triple will have to prove that the
      specific post-condition he wants can be lvs'd from whatever threaded together
      by magic wands. The library side, when proving seq_spec, will always have
@@ -69,9 +68,7 @@ Section atomic_sync.
     iIntros (f') "#Hsynced".
     iExists γ. iFrame.
     iIntros (x). iAlways.
-    rewrite /atomic_triple'.
     iIntros (P Q) "#Hvss".
-    rewrite /synced.
     iSpecialize ("Hsynced" $! P Q x).
     iIntros "!# HP". iApply wp_wand_r. iSplitL "HP".
     - iApply ("Hsynced" with "[]")=>//.
@@ -92,9 +89,8 @@ Section atomic_sync.
         apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. }
       iVs ("Hvs2" with "[Hg1 Hβ]").
       { iExists g'. iFrame. }
-      iVsIntro. iSplitL "Hg2 HÏ•'".
-      * iExists g'. by iFrame.
-      * done.
+      iVsIntro. iSplitL "Hg2 HÏ•'"; last done.
+      iExists g'. by iFrame.
     - iIntros (?) "?". by iExists g0.
   Qed.
 
diff --git a/flat.v b/flat.v
index 4213ca695c3bdb10c2feab34587b4d9e67c8db1d..3753263de335ad1608eab69578f97efc61b79986 100644
--- a/flat.v
+++ b/flat.v
@@ -1,3 +1,5 @@
+(* Flat Combiner *)
+
 From iris.program_logic Require Export weakestpre saved_prop.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
diff --git a/misc.v b/misc.v
index f916c4913619e14e978a0f979fd0e5f75428c304..3b3d2f23b0c260e5dfb40b477f49ef23a0ff64c5 100644
--- a/misc.v
+++ b/misc.v
@@ -1,35 +1,13 @@
+(* Miscellaneous lemmas *)
+
 From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Export lang proofmode notation.
 From iris.algebra Require Import auth frac gmap dec_agree upred_big_op.
 From iris.prelude Require Import countable.
 From iris.program_logic Require Import auth.
 Import uPred.
 
 Section lemmas.
-  Lemma op_some: ∀ {A: cmraT} (a b: A), Some a ⋅ Some b = Some (a ⋅ b).
-  Proof. done. Qed.
-
-  Lemma invalid_plus: ∀ (q: Qp), ¬ ✓ (1 + q)%Qp.
-  Proof.
-    intros q H.
-    apply (Qp_not_plus_q_ge_1 q).
-    done.
-  Qed.
-
-  Lemma pair_l_frac_update (g g': val):
-    ((1 / 2)%Qp, DecAgree g) â‹… ((1 / 2)%Qp, DecAgree g) ~~> ((1 / 2)%Qp, DecAgree g') â‹… ((1 / 2)%Qp, DecAgree g').
-  Proof.
-    repeat rewrite pair_op dec_agree_idemp.
-    rewrite frac_op' Qp_div_2.
-    eapply cmra_update_exclusive.
-    done.
-  Qed.
-  
-  Lemma pair_l_frac_op (p q: Qp) (g g': val):
-    (((p, DecAgree g') â‹… (q, DecAgree g'))) ~~> ((p + q)%Qp, DecAgree g').
-  Proof. by rewrite pair_op dec_agree_idemp frac_op'. Qed.
-
   Lemma pair_l_frac_op' (p q: Qp) (g g': val):
      ((p + q)%Qp, DecAgree g') ~~> (((p, DecAgree g') â‹… (q, DecAgree g'))).
   Proof. by rewrite pair_op dec_agree_idemp frac_op'. Qed.
diff --git a/simple_sync.v b/simple_sync.v
index 119277058ddaf7621b3007499b472a18b42429cd..861e678175fc0ad49c225a3bd81da4547691843d 100644
--- a/simple_sync.v
+++ b/simple_sync.v
@@ -1,6 +1,7 @@
+(* Coarse-grained syncer *)
+
 From iris.program_logic Require Export weakestpre hoare.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import dec_agree frac.
 From iris_atomic Require Import sync.
diff --git a/sync.v b/sync.v
index 7e8214217607e8321d4b6a3743f5714a74e36022..23cf7152faea4f67de1f98c5b4c578e662d3366e 100644
--- a/sync.v
+++ b/sync.v
@@ -1,3 +1,5 @@
+(* Syncer spec *)
+
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.