Commit 6d35edfe authored by Dan Frumin's avatar Dan Frumin
Browse files

Minor simplification

parent f62249a1
...@@ -22,7 +22,7 @@ Section test. ...@@ -22,7 +22,7 @@ Section test.
awp_load_ret x. awp_load_ret x.
iIntros (? ?) "[% Hx] [% Hx']"; simplify_eq/=. iIntros (? ?) "[% Hx] [% Hx']"; simplify_eq/=.
iExists _; eauto. repeat iSplit; eauto. iExists _; eauto. repeat iSplit; eauto.
iCombine "Hx Hx'" as "Hx". iFrame. by iFrame.
- iIntros (? ? ->) "[% Hx]"; simplify_eq/=. - iIntros (? ? ->) "[% Hx]"; simplify_eq/=.
iExists _; iFrame. eauto. iExists _; iFrame. eauto.
Qed. Qed.
......
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