Clean up the prerefinement proof

theories/logrel/contextual_refinement.v

+From iris.proofmode Require Import tactics.
 From iris_logrel.F_mu_ref_conc Require Export context_refinement.
 From iris_logrel.logrel Require Export fundamental_binary.
 From Autosubst Require Import Autosubst_Classes. (* for [subst] *)
@@ -52,6 +53,7 @@ Section bin_log_related_under_typed_ctx.
       => eapply (typed_X_closed Γ _ e H)
     end.
 
+  (* Precongruence *)
   Lemma bin_log_related_under_typed_ctx Γ e e' τ Γ' τ' K :
     (Closed (dom _ Γ) e) →
     (Closed (dom _ Γ) e') →
@@ -78,36 +80,27 @@ Section bin_log_related_under_typed_ctx.
         { by rewrite !dom_insert_binder. }
         eapply typed_ctx_closed; eauto.
         iAlways. iApply (IHK with "[Hrel]"); auto.
-      + iApply (bin_log_related_app with "[]").
+      + iApply (bin_log_related_app with "[]"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
-        fundamental.
       + iApply (bin_log_related_app _ _ _ _ _ _ _ τ2 with "[]"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_pair with "[]"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_pair with "[]"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply bin_log_related_fst; first by auto.
+      + iApply bin_log_related_fst; first done.
         iApply (IHK with "[Hrel]"); auto.
-      + iApply bin_log_related_snd; first by auto.
+      + iApply bin_log_related_snd; first done.
         iApply (IHK with "[Hrel]"); auto.
       + iApply bin_log_related_injl; first done.
         iApply (IHK with "[Hrel]"); auto.
       + iApply bin_log_related_injr; first done.
         iApply (IHK with "[Hrel]"); auto.
-      + inversion Hx2; subst.
-        * iApply (bin_log_related_case with "[] []"); try fundamental.
-        * iApply (bin_log_related_case with "[] []"); try fundamental.
-          iApply (IHK with "[Hrel]"); auto.
-      + match goal with
-          H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst
-        end.
-        iApply (bin_log_related_case with "[] []"); try fundamental.
-        iApply (IHK with "[Hrel]"); auto.
-      + match goal with
-          H : typed_ctx_item _ _ _ _ _ |- _ => inversion H; subst
-        end.
-        iApply (bin_log_related_case with "[] []"); try fundamental.
+      + iApply (bin_log_related_case with "[] []"); try fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_case with "[] []"); try fundamental.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_case with "[] []"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_if with "[] []"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.

theories/logrel/soundness_binary.v

@@ -52,7 +52,6 @@ Proof.
     iIntros "!> !%"; eauto.
 Qed.
 
-
 Theorem logrel_typesafety Σ `{logrelPreG Σ} Δ e e' τ thp σ σ' :
   (∀ `{logrelG Σ}, {⊤,⊤;Δ;∅} ⊨ e ≤log≤ e : τ) →
   rtc step ([e], σ) (thp, σ') → e' ∈ thp →