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

Nits

parent 2c1e72c3
No related branches found
No related tags found
1 merge request!5n-ary choice
Hide whitespace changes
Inline Side-by-side
theories/logrel/subtyping.v
+ 2
− 2
View file @ 20ce8454
...@@ -242,7 +242,7 @@ Section subtype. ...@@ -242,7 +242,7 @@ Section subtype.
Ps2 ⊆ Ps1 → Ps2 ⊆ Ps1 →
⊢ lsty_select Ps1 <p: lsty_select Ps2. ⊢ lsty_select Ps1 <p: lsty_select Ps2.
Proof. Proof.
iIntros (Hnone) "!>". iIntros (Hsub) "!>".
iApply iProto_le_send. iApply iProto_le_send.
iIntros (x) ">% !>"=> /=. iIntros (x) ">% !>"=> /=.
iExists _. iSplit=> //. iExists _. iSplit=> //.
...@@ -279,7 +279,7 @@ Section subtype. ...@@ -279,7 +279,7 @@ Section subtype.
Ps1 ⊆ Ps2 → Ps1 ⊆ Ps2 →
⊢ lsty_branch Ps1 <p: lsty_branch Ps2. ⊢ lsty_branch Ps1 <p: lsty_branch Ps2.
Proof. Proof.
iIntros (Hnone) "!>". iIntros (Hsub) "!>".
iApply iProto_le_recv. iApply iProto_le_recv.
iIntros (x) ">% !>"=> /=. iIntros (x) ">% !>"=> /=.
iExists _. iSplit=> //. iExists _. iSplit=> //.
......
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