Simplify the `bin_log_related_val` proof

theories/logrel/rules.v

@@ -20,14 +20,10 @@ Section properties.
     to_val e' = Some v' →
     (|={E}=> ⟦ τ ⟧ Δ (v, v')) ⊢ {E;Δ;Γ} ⊨ e ≤log≤ e' : τ.
   Proof.
-    rewrite bin_log_related_eq.
-    iIntros (Hv Hv') "IH".
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    replace e with (of_val v); auto using of_to_val.
-    replace e' with (of_val v'); auto using of_to_val.
-    rewrite /env_subst !Closed_subst_p_id.
-    iMod "IH" as "IH".
-    iModIntro. iApply wp_value; eauto.
+    iIntros (He He') "Hτ".
+    iMod "Hτ" as "Hτ".
+    rewrite (interp_ret E); eauto.
+    by rewrite -related_ret.
   Qed.
 
   Lemma bin_log_related_arrow_val Δ Γ E (f x f' x' : binder) (e e' eb eb' : expr) (τ τ' : type) :