diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index c677894b63ae0cf4bf4d9810c6c15f4610029d53..aeb91c9d682e1c6239b24d9e652bf4c57d9e8b7a 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -45,7 +45,4 @@ End bit_refinement.
 
 Theorem bit_ctx_refinement :
   ∅ ⊨ bit_bool ≤ctx≤ bit_nat : bitτ.
-Proof.
-  eapply (refines_sound relocΣ).
-  iIntros (? Δ). iApply (bit_refinement Δ).
-Qed.
+Proof. auto using (refines_sound relocΣ), bit_refinement. Qed.