diff --git a/theories/examples/ro_test.v b/theories/examples/ro_test.v
new file mode 100644
index 0000000000000000000000000000000000000000..9ed16d98c8b674e445350f03969b3455124ae754
--- /dev/null
+++ b/theories/examples/ro_test.v
@@ -0,0 +1,29 @@
+From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import tactics.
+From igps Require Import persistor fractor notation weakestpre ro na invariants proofmode ghosts.
+Import uPred lang.base.
+
+Section test.
+  Context `{fG : foundationG Σ}
+          `{persG : persistorG Σ}
+          {cG : cancelable_invariants.cinvG Σ}.
+
+Lemma test N l v V (HN: ↑physN ∪ ↑fracN ## namespaces.nclose N):
+  {{{ ⎡PSCtx⎤ ∗ inv N (own_loc_ro l v V) ∗ monPred_in V }}} [ #l]_na {{{ RET #v; emp }}}.
+Proof.
+  intros; iIntros "(#kI & #inv & in) Hpost".
+  iMod (inv_open with "inv") as "[oL Hclose]"; first done.
+  iMod (timeless with "oL") as "oL".
+  { admit. }
+  iPoseProof (all_now with "oL") as "oL".
+  iPoseProof (ro_split with "[$in $oL]") as "[oL oL']".
+  iDestruct "oL'" as (q) "oL'".
+  apply disjoint_union_l in HN as [].
+  iApply (na_read_frac with "[$]").
+  { by apply namespaces.ndisj_subseteq_difference. }
+  { etrans; first apply namespaces.nclose_subseteq.
+    by apply namespaces.ndisj_subseteq_difference. }
+  iNext; iIntros (?) "[% oL']"; subst.
+  iMod ("Hclose" with "[oL]"); first by iApply objective_all.
+  iApply "Hpost"; auto.
+Admitted.
\ No newline at end of file
diff --git a/theories/invariants.v b/theories/invariants.v
index d0e0ec1e28fe073bcf3d50d98b02f9478b035e15..aedb5230eb582d6b2ce206f4344142a16d1e43c7 100644
--- a/theories/invariants.v
+++ b/theories/invariants.v
@@ -5,55 +5,10 @@ From igps Require Import ghosts viewpred ro.
 
 Section Invariants.
   Context {Σ : gFunctors} `{fG : !foundationG Σ} `{W : invG.invG Σ}.
-  Definition inv_def : namespaces.namespace → vProp Σ → vProp Σ :=
-    λ N P, MonPred (λ _, invariants.inv N (∀ V, monPred_at P V))%I _.
-  Definition inv_aux : seal (@inv_def). by eexists. Qed.
-  Definition inv := unseal (@inv_aux).
-  Definition inv_eq : inv = _ := seal_eq _.
-
-  Definition inv_contractive : ∀ N (n : nat), Proper (dist_later n ==> dist n) (inv N).
-  Proof.
-    intros. rewrite inv_eq /inv_def /=. intros ? ? ? => /=.
-    split => ?.
-    refine (invariants.inv_contractive _ _ _ _ _).
-    destruct n => //.
-    cbn in *. apply bi.forall_ne.
-    intros ?. apply H.
-  Qed.
-
-  Global Instance inv_ne  : ∀ N (n : nat), Proper (dist n ==> dist n) (inv N).
-  Proof.
-    rewrite inv_eq /inv_def /=. intros.
-    intros ? ? ? => /=. split => ?.
-    apply invariants.inv_ne.
-    apply bi.forall_ne.
-    intros ?. apply H.
-  Qed.
-
-  Global Instance inv_Proper : ∀ N, Proper (equiv ==> equiv) (inv N).
-  Proof.
-    intros.
-    rewrite inv_eq /inv_def /=. intros.
-    intros ? ? ? => /=. split => ?.
-    apply invariants.inv_Proper.
-    apply bi.forall_proper.
-    intros ?. apply H.
-  Qed.
-
-  Global Instance inv_persistent : ∀ N (P : vProp Σ), Persistent (inv N P).
-  Proof.
-    intros.
-    rewrite inv_eq /inv_def /=. intros.
-    split => ?.
-    rewrite /Persistent /=.
-    rewrite {1}invariants.inv_persistent.
-    unfold bi_persistently.
-    iStartProof (uPred _). by iIntros "#? !#".
-  Qed.
+  Definition inv N (P : vProp Σ) : vProp Σ := ⎡invariants.inv N (∀ V, monPred_at P V)⎤%I.
 
   Lemma inv_alloc N (E : coPset) (P : vProp Σ) : ▷ (ɐ P) -∗ |={E}=> inv N P.
   Proof.
-    rewrite inv_eq /inv_def /=.
     iStartProof (uPred _). iIntros (V) "H".
     iMod (invariants.inv_alloc with "H") as "H".
     iModIntro. by rewrite monPred_all_eq.
@@ -62,7 +17,6 @@ Section Invariants.
   Lemma inv_alloc_open N (E : coPset) (P : vProp Σ) :
     ↑N ⊆ E → (|={E,E ∖ ↑N}=> inv N P ∗ (▷ (ɐ P) ={E ∖ ↑N,E}=∗ True))%I.
   Proof.
-    rewrite inv_eq /inv_def /=.
     intros.
     iStartProof (uPred _). iIntros.
     iPoseProof (invariants.inv_alloc_open) as "T"; [done|].
@@ -73,7 +27,6 @@ Section Invariants.
  Lemma inv_open (E : coPset) N (P : vProp Σ) :
    ↑N ⊆ E → inv N P -∗ |={E,E ∖ ↑N}=> ▷ (ɐ P) ∗ (▷ (ɐ P) ={E ∖ ↑N,E}=∗ True).
  Proof.
-    rewrite inv_eq /inv_def /=.
     intros.
     iStartProof (uPred _). iIntros (?) "H".
     iPoseProof (invariants.inv_open with "H") as "T"; [done|].
@@ -164,11 +117,6 @@ Section Invariants.
  Global Instance wand_objective P Q (H : P -∗ Q) : Objective (P -∗ Q)%I.
  Proof. iStartProof (uPred _). iIntros (??) "H %% HP". by iApply H. Qed.
 
- Global Instance own_loc_ro_objective l v V: Objective (own_loc_ro l v V)%I.
- Proof.
-   iStartProof (uPred _). auto.
- Qed.
-
  Lemma all_entails (P Q : vProp Σ) : (P -∗ Q) -> bi_valid (ɐ (P -∗ Q))%I.
  Proof.
   intro; iIntros.
diff --git a/theories/ro.v b/theories/ro.v
index 657a8edb9624e9bb1fd076819a132b071ae04cf2..786ae436c1fcee4253a5c3eba3965590c3e5745b 100644
--- a/theories/ro.v
+++ b/theories/ro.v
@@ -16,21 +16,4 @@ Section RO.
    iDestruct "oL2" as (V') "[??]"; eauto.
  Qed.
 
- Lemma ro_join l v V q' v': own_loc_ro l v V ∗ l ↦{q'} v' ={↑fracN.@l}=∗ own_loc_ro l v V.
- Proof.
-   iStartProof (uPred _).
-   iIntros (i) "[oL oL']"; iDestruct "oL" as (q) "oL".
-   iExists (q + q')%Qp.
-   iApply (na_frac_join with "[>-]").
-   rewrite /own_loc_na_frac valloc_local_eq /=.
-   iDestruct "oL" as (V0) "[% oL]"; iDestruct "oL'" as (V') "[% oL']".
-(*   iMod (fractor_open with "oL") as (?) "(? & ? & ?)"; first done.*)
-   iAssert (⌜V0 = V'⌝)%I as %?.
-   { admit. }
-   iAssert ⌜v = v'⌝%I as %?.
-   { iPoseProof (fractor_join_l with "[$oL $oL']") as "oL".
-     iDestruct "oL" as (?) "[[%%] _]"; subst.
-     apply encode_inj in H4; inversion H4; done. }
-   subst; iSplitL "oL"; eauto.
- Admitted.   
-End RO.
\ No newline at end of file
+End RO.