Commit 0657f6bf authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Stuck.

parent 741c78cf
......@@ -118,7 +118,7 @@ Section has_type.
WP ν @ E {{ Φ }}.
Proof.
iIntros "H◁ HΦ". setoid_rewrite has_type_value. unfold has_type.
destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]".
destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]". simpl.
iMod ("HΦ" $! v with "[] H◁") as "HΦ". done.
iInduction ν as [| | |[] e ? [|[]| | | | | | | | | |] _| | | | | | | |] "IH"
forall (Φ v EQν); try done.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment