diff --git a/diaframe/steps/introduce_hyp.v b/diaframe/steps/introduce_hyp.v
index 9c8f388d34f5ebd824ee153f8c15ad77a5249428..f0bf49f32c0e739574f1a6881f89a5b7ca2dafd0 100644
--- a/diaframe/steps/introduce_hyp.v
+++ b/diaframe/steps/introduce_hyp.v
@@ -295,21 +295,6 @@ Section coq_tactics.
     rewrite HΔ //.
   Qed.
 
-  Global Instance mergable_persist_from_box P p P2 P3 :
-    MergePersist P p P2 P3 →
-    MergePersist (□ P)%I p P2 P3 | 5.
-  Proof.
-    rewrite /MergePersist => <-.
-    iIntros "[#$ $]".
-  Qed.
-  Global Instance mergable_consume_from_box P p P2 P3 :
-    MergeConsume P p P2 P3 →
-    MergeConsume (□ P)%I p P2 P3 | 5.
-  Proof.
-    rewrite /MergeConsume => <-.
-    iIntros "[#$ $]".
-  Qed.
-
   Lemma tac_introduce_hyp_not_mergable j Δ P1 a P1' R : 
     TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
         (TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) →
diff --git a/diaframe/steps/solve_instances.v b/diaframe/steps/solve_instances.v
index 48f3ee40847f1ddce5b9c372ccf23790b4888184..f8c38ed80ead003475a44edaac8fcd9d13c00434 100644
--- a/diaframe/steps/solve_instances.v
+++ b/diaframe/steps/solve_instances.v
@@ -213,17 +213,34 @@ End drop_modal_instances.
 
 Section misc.
   Context {PROP : bi}.
+  Implicit Types P Q : PROP.
   (* TODO: where to put this? *)
 
-  Global Instance exclusive_prop_try_merge (Q : PROP) :
+  Global Instance exclusive_prop_try_merge Q :
     ExclusiveProp Q → TryMerge Q.
   Proof. exact (λ _, I). Qed.
 
-  Global Instance exclusive_prop_merge_false (Q : PROP) p : 
+  Global Instance exclusive_prop_merge_false Q p : 
     ExclusiveProp Q →
     MergeConsume Q p Q False%I.
   Proof.
     rewrite /ExclusiveProp /MergeConsume bi.intuitionistically_if_elim //.
   Qed.
+
+  Global Instance mergable_persist_from_box P p P2 P3 :
+    MergePersist P p P2 P3 →
+    MergePersist (□ P)%I p P2 P3 | 5.
+  Proof.
+    rewrite /MergePersist => <-.
+    iIntros "[#$ $]".
+  Qed.
+  Global Instance mergable_consume_from_box P p P2 P3 :
+    MergeConsume P p P2 P3 →
+    MergeConsume (□ P)%I p P2 P3 | 5.
+  Proof.
+    rewrite /MergeConsume => <-.
+    iIntros "[#$ $]".
+  Qed.
+  Global Instance try_merge_from_box P : TryMerge P → TryMerge (□ P)%I := id.
 End misc.