From e82a0c75ef639aeee9bf7c3c988b43f4ec789f2d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 15 Jun 2020 18:46:37 +0200
Subject: [PATCH] Tweak.

---
 theories/examples/bit.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index c677894..aeb91c9 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.
-- 
GitLab