more line breaks and a let-lemma specifically for values

theories/opt/ex1.v

@@ -37,5 +37,9 @@ Proof.
   apply sim_body_init_call. simpl.
 
   (* Alloc *)
-  sim_bind (Alloc _) (Alloc _).
+  sim_bind (Alloc _) (Alloc _). simpl.
+  apply sim_body_alloc_shared. simpl. intros -> ->.
+
+  (* Let *)
+  sim_bind (Let _ _ _) (Let _ _ _).
 Abort.

theories/sim/instance.v

@@ -3,7 +3,7 @@ From stbor.sim Require Export local invariant.
 
 Notation "r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ" :=
   (sim_local_body wsat vrel_expr fs ft r n%nat es%E σs et%E σt Φ)
-  (at level 70, format "'[hv' r  ⊨{ n , fs , ft } '/  ' '[  ' ( es ,  σs ) ']' '/' ≥  '/  ' '[  ' ( et ,  σt ) ']'  '/' :  Φ ']'").
+  (at level 70, format "'[hv' r  '/' ⊨{ n , fs , ft } '/  ' '[ ' ( es ,  '/' σs ) ']' '/' ≥  '/  ' '[ ' ( et ,  '/' σt ) ']'  '/' :  Φ ']'").
 
 Notation "⊨{ fs , ft } f1 ≥ᶠ f2" :=
   (sim_local_fun wsat vrel_expr fs ft end_call_sat f1 f2)

theories/sim/refl_step.v

@@ -1149,6 +1149,11 @@ Proof.
   split; [done|]. by left.
 Qed.
 
+Lemma sim_body_let_val fs ft r n x (vs1 vt1: value) es2 et2 σs σt Φ :
+  r ⊨{n,fs,ft} (subst x vs1 es2, σs) ≥ (subst x vt1 et2, σt) : Φ →
+  r ⊨{n,fs,ft} (let: x := vs1 in es2, σs) ≥ ((let: x := vt1 in et2), σt) : Φ.
+Proof. apply sim_body_let; eauto. Qed.
+
 (** Ref *)
 Lemma sim_body_ref fs ft r n l tgs tgt Ts Tt σs σt Φ :
   r ⊨{n,fs,ft} (#[ScPtr l tgs], σs) ≥ (#[ScPtr l tgt], σt) : Φ →