Commit af4a0111 authored by Dan Frumin's avatar Dan Frumin

Clean up translation.v

parent ab69de42
...@@ -495,9 +495,8 @@ Section proofs. ...@@ -495,9 +495,8 @@ Section proofs.
iIntros (v1 v2) "Hv1 Hv2 !>". awp_let. iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
iDestruct ("Hv2" with "Hv1") as ([pl pi] [ql qi] -> ->) "HΦ /=". iDestruct ("Hv2" with "Hv1") as ([pl pi] [ql qi] -> ->) "HΦ /=".
do 2 (awp_proj; awp_let). do 2 awp_proj. do 2 (awp_proj; awp_let). do 2 awp_proj.
unfold cloc_lt; simpl. case_bool_decide as Hp; awp_op. unfold cloc_lt; simpl. case_bool_decide as Hp; subst; awp_op.
- destruct Hp as [-> ?%Nat2Z.inj_lt]. - rewrite (bool_decide_true (LitV ql = LitV ql)) //. awp_if. do 2 awp_proj.
rewrite (bool_decide_true (LitV pl = LitV pl)) //. awp_if. do 2 awp_proj.
iApply awp_ret. wp_op. iApply awp_ret. wp_op.
rewrite (bool_decide_iff (pi < qi)%nat (pi < qi)); eauto using Nat2Z.inj_lt. rewrite (bool_decide_iff (pi < qi)%nat (pi < qi)); eauto using Nat2Z.inj_lt.
- rewrite bool_decide_false; last congruence. - rewrite bool_decide_false; last congruence.
......
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