Skip to content
Snippets Groups Projects
Commit d20b3324 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Nit

parent 8769e41e
No related branches found
No related tags found
No related merge requests found
Pipeline #27511 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/logrel/subtyping_rules.v
+ 1
− 1
View file @ d20b3324
......@@ -298,7 +298,7 @@ Section subtyping_rules.
iApply iProto_le_trans;
[iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ x2)|]; simpl.
iApply iProto_le_payload_elim_r.
iMod 1 as "%". revert H1.
iMod 1 as %HSs. revert HSs.
rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
iApply iProto_le_trans; [iApply iProto_le_base_swap|]. iSplitL; [by eauto|].
iModIntro. by iExists v1.
......
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