name mangling

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 _ _ _ _ _ τ1); done.
-    - iApply (bin_log_related_app _ _ _ _ _ τ1); 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.