diff --git a/lifetime.v b/lifetime.v
index a4b579eff22d7a0abe6162e08d358d830f047451..ae6e905adc641d44a307def39311cf81dfbf0ff5 100644
--- a/lifetime.v
+++ b/lifetime.v
@@ -61,7 +61,8 @@ Section lft.
   Global Existing Instance lft_incl_persistent.
 
   Axiom lft_extract_proper : ∀ κ, Proper ((⊣⊢) ==> (⊣⊢)) (lft_extract κ).
-  Global Existing Instance lft_extract_proper.
+  Axiom lft_extract_mono : ∀ κ, Proper ((⊢) ==> (⊢)) (lft_extract κ).
+  Global Existing Instances lft_extract_proper lft_extract_mono.
 
   Axiom lft_borrow_proper : ∀ κ, Proper ((⊣⊢) ==> (⊣⊢)) (lft_borrow κ).
   Global Existing Instance lft_borrow_proper.
diff --git a/perm_incl.v b/perm_incl.v
index 83e7be59bc5884fd4a9f71c12435f985f1d33f50..3f46d966792326b1979f8a850c93cfabb00d4876 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -238,10 +238,8 @@ Section props.
       - iExists _. eauto. }
     iVs (lft_borrow_create with "Hκ Hf") as "[_ Hf]". done.
     iVs (lft_extract_combine with "[-]"). done. by iFrame.
-    (* FIXME : extraction needs to be monotone in some sense to
-       remove the later. *)
-    admit.
-  Admitted.
+    iVsIntro. iApply lft_extract_mono; last done. by iDestruct 1 as "[$$]".
+  Qed.
 
   Lemma reborrow_uniq_borrowing κ κ' v ty :
     borrowing κ (κ ⊑ κ') (v ◁ &uniq{κ'}ty) (v ◁ &uniq{κ}ty).