diff --git a/theories/logrel/F_mu_ref_conc/binary/fundamental.v b/theories/logrel/F_mu_ref_conc/binary/fundamental.v
index 497cf8856df3bdbb3526800611ca495601a406a1..7d8696af6e8e9ddf6a7a33d167f1cca4115e7f4b 100644
--- a/theories/logrel/F_mu_ref_conc/binary/fundamental.v
+++ b/theories/logrel/F_mu_ref_conc/binary/fundamental.v
@@ -560,36 +560,38 @@ Section fundamental.
   Theorem binary_fundamental Γ e τ :
     Γ ⊢ₜ e : τ → ⊢ Γ ⊨ e ≤log≤ e : τ.
   Proof.
-    induction 1.
-    - iApply bin_log_related_var; done.
+    elim=> {}Γ {e τ}.
+    - intros; iApply bin_log_related_var; done.
     - iApply bin_log_related_unit.
-    - iApply bin_log_related_int.
-    - iApply bin_log_related_bool.
-    - iApply bin_log_related_int_binop; done.
-    - iApply bin_log_related_Eq_binop; done.
-    - iApply bin_log_related_pair; done.
-    - iApply bin_log_related_fst; done.
-    - iApply bin_log_related_snd; done.
-    - iApply bin_log_related_injl; done.
-    - iApply bin_log_related_injr; done.
-    - iApply bin_log_related_case; done.
-    - iApply bin_log_related_if; done.
-    - iApply bin_log_related_rec; done.
-    - iApply bin_log_related_lam; done.
-    - iApply bin_log_related_letin; done.
-    - iApply bin_log_related_seq; done.
-    - iApply bin_log_related_app; done.
-    - iApply bin_log_related_tlam; done.
-    - iApply bin_log_related_tapp; done.
-    - iApply bin_log_related_pack; done.
-    - iApply bin_log_related_unpack; done.
-    - iApply bin_log_related_fold; done.
-    - iApply bin_log_related_unfold; done.
-    - iApply bin_log_related_fork; done.
-    - iApply bin_log_related_alloc; done.
-    - iApply bin_log_related_load; done.
-    - iApply bin_log_related_store; done.
-    - iApply bin_log_related_CAS; done.
-    - iApply bin_log_related_FAA; done.
+    - intros; iApply bin_log_related_int.
+    - intros; iApply bin_log_related_bool.
+    - intros; iApply bin_log_related_int_binop; done.
+    - intros; iApply bin_log_related_Eq_binop; done.
+    - intros; iApply bin_log_related_pair; done.
+    - intros; iApply bin_log_related_fst; done.
+    - intros; iApply bin_log_related_snd; done.
+    - intros; iApply bin_log_related_injl; done.
+    - intros; iApply bin_log_related_injr; done.
+    - intros; iApply bin_log_related_case; done.
+    - intros; iApply bin_log_related_if; done.
+    - intros; iApply bin_log_related_rec; done.
+    - intros; iApply bin_log_related_lam; done.
+    - intros; iApply bin_log_related_letin; done.
+    - move=> e1 e2 Ï„1 Ï„2 ? ? ? ?.
+      iApply (bin_log_related_seq _ _ _ _ _ Ï„1); done.
+    - move=> e1 e2 Ï„1 Ï„2 ? ? ? ?.
+      iApply (bin_log_related_app _ _ _ _ _ Ï„1); done.
+    - intros; iApply bin_log_related_tlam; done.
+    - intros; iApply bin_log_related_tapp; done.
+    - intros; iApply bin_log_related_pack; done.
+    - intros; iApply bin_log_related_unpack; done.
+    - intros; iApply bin_log_related_fold; done.
+    - intros; iApply bin_log_related_unfold; done.
+    - intros; iApply bin_log_related_fork; done.
+    - intros; iApply bin_log_related_alloc; done.
+    - intros; iApply bin_log_related_load; done.
+    - move=> e1 e2 Ï„ ? ? ? ?; iApply (bin_log_related_store _ _ _ _ _ Ï„); done.
+    - intros; iApply bin_log_related_CAS; done.
+    - intros; iApply bin_log_related_FAA; done.
   Qed.
 End fundamental.