wip on correctness of vcg_wp

theories/vcgen/vcgen.v

@@ -334,7 +334,9 @@ Lemma vcg_inhale_list_sound' E s t :
     - iIntros "H".
       remember (vcg_sp E s de1) as sp. symmetry in Heqsp.
       destruct sp as [[[s1 s2] dv]|]; last first.
-      { simpl.  admit. (* TODO: incorrect *) }
+      {  iApply (awp_wand with "H").
+      iIntros (v) "H". iExists (dValUnknown v).
+      eauto 30 with iFrame.  }
       rewrite vcg_inhale_list_sound'.
       iDestruct "H" as "[Henv Hde2]".
       rewrite IHde2.
@@ -353,7 +355,7 @@ Lemma vcg_inhale_list_sound' E s t :
       iSplit.
       iPureIntro. by apply dbin_op_eval_correct.
       eauto with iFrame.
-  Admitted.
+  Qed.
 
   Lemma tac_vcg_sound Γs_in Γs_out Γls Γp ps c e R Φ E F dce :
     MapstoListFromEnv Γs_in Γs_out Γls →