diff --git a/perm.v b/perm.v
index da600e7fea39217c12357ee4af0a757a436f51c7..b4c0a98c6962895d669dbe858ffbd6fbef2615d6 100644
--- a/perm.v
+++ b/perm.v
@@ -79,4 +79,4 @@ Section duplicable.
   Global Instance top_dup : Duplicable ⊤.
   Proof. intros tid. apply _. Qed.
 
-End duplicable.
\ No newline at end of file
+End duplicable.
diff --git a/type.v b/type.v
index b35b238a4f73c5d9e11ec181576b4b7812a93e4b..3e916c8d1ce45f355c8cd7aa0d281f91641fd681 100644
--- a/type.v
+++ b/type.v
@@ -55,6 +55,10 @@ Section defs.
   Program Definition ty_of_st (st : simple_type) : type :=
     {| ty_size := st.(st_size); ty_dup := true;
        ty_own := st.(st_own);
+
+       (* [st.(st_own) tid vl] needs to be outside of the fractured
+          borrow, otherwise I do not knwo how to prove the shr part of
+          [lft_incl_ty_incl_shared_borrow]. *)
        ty_shr := λ κ tid _ l,
                  (∃ vl, (&frac{κ} λ q, l ↦★{q} vl) ★ ▷ st.(st_own) tid vl)%I
     |}.