Added left/right rules to dual subtyping

theories/channel/proto.v

@@ -797,6 +797,20 @@ Section proto.
       iNext. by iRewrite "Hp2d".
   Qed.
 
+  Lemma iProto_le_dual_l p1 p2 :
+    iProto_le (iProto_dual p2) p1 -∗ iProto_le (iProto_dual p1) p2.
+  Proof.
+    iIntros "H". iEval (rewrite -(iProto_dual_involutive p2)).
+    by iApply iProto_le_dual.
+  Qed.
+
+  Lemma iProto_le_dual_r p1 p2 :
+    iProto_le p2 (iProto_dual p1) -∗ iProto_le p1 (iProto_dual p2).
+  Proof.
+    iIntros "H". iEval (rewrite -(iProto_dual_involutive p1)).
+    by iApply iProto_le_dual.
+  Qed.
+
   Lemma iProto_le_app p1 p2 p3 p4 :
     iProto_le p1 p2 -∗ iProto_le p3 p4 -∗ iProto_le (p1 <++> p3) (p2 <++> p4).
   Proof.

theories/logrel/subtyping.v

@@ -295,6 +295,12 @@ Section subtype.
   Lemma lsty_le_dual S1 S2 : S2 <s: S1 -∗ lsty_dual S1 <s: lsty_dual S2.
   Proof. iIntros "#H !>". by iApply iProto_le_dual. Qed.
 
+  Lemma lsty_le_dual_l S1 S2 : lsty_dual S2 <s: S1 -∗ lsty_dual S1 <s: S2.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual_l. Qed.
+
+  Lemma lsty_le_dual_r S1 S2 : S2 <s: lsty_dual S1 -∗ S1 <s: lsty_dual S2.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual_r. Qed.
+
   Lemma lsty_le_rec_1 (C : lsty Σ → lsty Σ) `{!Contractive C} :
     ⊢ lsty_rec C <s: C (lsty_rec C).
   Proof.