diff --git a/srv.v b/srv.v
index ed42605517e6d5356b46ce65d3c7c405e3b9d901..c6ec99e1aefd5ca812fe84556ab77855e747a7d1 100644
--- a/srv.v
+++ b/srv.v
@@ -34,22 +34,7 @@ Definition mk_srv : val :=
         release "l";;
         "ret".
 
-(* play with some algebraic structure to see what fit ... *)
-
 Definition srvR := prodR fracR (dec_agreeR val).
-
-Lemma srv_coincide: ∀ (x1 x2: val) (q1 q2: Qp), ✓ ((q1, DecAgree x1) ⋅ (q2, DecAgree x2)) → x1 = x2.
-Proof.
-  intros x1 x2 q1 q2 H. destruct (decide (x1 = x2))=>//.
-  exfalso. destruct H as [H1 H2].
-  simpl in H2. apply dec_agree_op_inv in H2.
-  by inversion H2.
-Qed.
-
-Lemma srv_update: ∀ (x1 x2: val), (1%Qp, DecAgree x1) ~~> (1%Qp, DecAgree x2).
-Proof. intros. by apply cmra_update_exclusive. Qed.
-
-(* define the gFunctors *)
 Class srvG Σ := FlatG { srv_tokG :> inG Σ srvR }.
 Definition srvΣ : gFunctors := #[GFunctor (constRF srvR)].
 
diff --git a/sync.v b/sync.v
index 0d40bb02deaa5a2d32494fbc1f91178597ffe300..9b6111d97650f0af49a9c5345056dfeb961a8de6 100644
--- a/sync.v
+++ b/sync.v
@@ -106,7 +106,7 @@ Section generic.
   Definition gFrag (γ: gname) g : iProp Σ := own γ (gFragR g).
   Definition gFull (γ: gname) g : iProp Σ := own γ (gFullR g).
   
-  Global Instance frag_timeless γ g: TimelessP (@own Σ syncR sync_tokG γ (gFragR g)).
+  Global Instance frag_timeless γ g: TimelessP (gFrag γ g).
   Proof. apply _. Qed.
 
   Global Instance full_timeless γ g: TimelessP (gFull γ g).