diff --git a/tests/one_shot.ref b/tests/one_shot.ref
index 08d4ddb27e054a71e9484fbc5f201125f9eeedb5..c06e1621c61a96598a4f9583800380f048216bfa 100644
--- a/tests/one_shot.ref
+++ b/tests/one_shot.ref
@@ -40,3 +40,4 @@
                     | InjR "m" => assert: #m = "m"
                     end {{ _, True }}
   
+Closed under the global context
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 37fcbef63f0aecfae813fbe5b0cabb55b033e10e..a71159b6a60196eaad21b111c83927fe963bc0a2 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -1,8 +1,9 @@
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl agree csum.
-From iris.heap_lang Require Import assert proofmode notation.
+From iris.heap_lang Require Import assert proofmode notation adequacy.
 From iris.proofmode Require Import tactics.
+From iris.heap_lang.lib Require Import par.
 Set Default Proof Using "Type".
 
 Definition one_shot_example : val := λ: <>,
@@ -95,3 +96,35 @@ Proof.
   - iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
 Qed.
 End proof.
+
+(* Have a client with a closed proof. *)
+Definition client : expr :=
+  let: "ff" := one_shot_example #() in
+  (Fst "ff" #5 ||| let: "check" := Snd "ff" #() in "check" #()).
+
+Section client.
+  Local Set Default Proof Using "Type*".
+  Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
+
+  Lemma client_safe : WP client {{ _, True }}%I.
+  Proof.
+    rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]".
+    wp_let. wp_apply wp_par.
+    - wp_apply "Hf1".
+    - wp_proj. wp_bind (f2 _)%E. iApply wp_wand; first by iExact "Hf2".
+      iIntros (check) "Hcheck". wp_pures. iApply "Hcheck".
+    - auto.
+  Qed.
+End client.
+
+(** Put together all library functors. *)
+Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
+(** This lemma implicitly shows that these functors are enough to meet
+all library assumptions. *)
+Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
+Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
+
+(* Since we check the output of the test files, this means
+our test suite will fail if we ever accidentally add an axiom
+to anything used by this proof. *)
+Print Assumptions client_adequate.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 536fbbc6cd8c4bba5b686121cd38f493b18980b5..f7672c263c6b1ec6c4c3eebe8b642ff2260d01a5 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -683,6 +683,7 @@ Bind Scope cFunctor_scope with cFunctor.
 
 Class cFunctorContractive (F : cFunctor) :=
   cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).
+Hint Mode cFunctorContractive ! : typeclass_instances.
 
 Definition cFunctor_diag (F: cFunctor) (A: ofeT) : ofeT := cFunctor_car F A A.
 Coercion cFunctor_diag : cFunctor >-> Funclass.