Clean up.

theories/logrel/subtyping.v

@@ -295,58 +295,50 @@ Section subtype.
   Lemma lsty_le_app_assoc_l S1 S2 S3 :
     ⊢ S1 <++> (S2 <++> S3) <s: (S1 <++> S2) <++> S3.
   Proof. rewrite assoc. iApply lsty_le_refl. Qed.
-
   Lemma lsty_le_app_assoc_r S1 S2 S3 :
     ⊢ (S1 <++> S2) <++> S3 <s: S1 <++> (S2 <++> S3).
   Proof. rewrite assoc. iApply lsty_le_refl. Qed.
 
-  Lemma lsty_le_app_id_l_l S :
-    ⊢ (END <++> S) <s: S.
+  Lemma lsty_le_app_id_l_l S : ⊢ (END <++> S) <s: S.
   Proof. rewrite left_id. iApply lsty_le_refl. Qed.
-
-  Lemma lsty_le_app_id_l_r S :
-    ⊢ (S <++> END) <s: S.
+  Lemma lsty_le_app_id_l_r S : ⊢ (S <++> END) <s: S.
   Proof. rewrite right_id. iApply lsty_le_refl. Qed.
-
-  Lemma lsty_le_app_id_r_l S :
-    ⊢ S <s: (END <++> S).
+  Lemma lsty_le_app_id_r_l S : ⊢ S <s: (END <++> S).
   Proof. rewrite left_id. iApply lsty_le_refl. Qed.
-
-  Lemma lsty_le_app_id_r_r S :
-    ⊢ S <s: (S <++> END).
+  Lemma lsty_le_app_id_r_r S : ⊢ S <s: (S <++> END).
   Proof. rewrite right_id. iApply lsty_le_refl. Qed.
 
   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_send_l A S : ⊢ (lsty_dual (<!!>A;S)) <s: (<??>A;(lsty_dual S)).
-  Proof.
-    rewrite /lsty_le /lsty_dual /lsty_send /lsty_recv /lsty_message iProto_dual_message /=.
-    iIntros "!>".
-    rewrite {1}/lsty_car /=.
-    iApply iProto_le_refl.
-  Admitted.
-
-  Lemma lsty_le_dual_send_r A S : ⊢ (<!!>A;(lsty_dual S)) <s: lsty_dual (<??> A;S).
-  Proof. Admitted.
-
-  Lemma lsty_le_dual_recv_l A S : ⊢ (lsty_dual (<??> A;S)) <s: (<!!> A;(lsty_dual S)).
-  Proof. Admitted.
-  Lemma lsty_le_dual_recv_r A S : ⊢ (<??>A;(lsty_dual S)) <s: lsty_dual (<!!> A;S).
-  Proof. Admitted.
-
-  Lemma lsty_le_dual_end_l : ⊢ (lsty_dual (Σ:=Σ) END) <s: END.
-  Proof. rewrite /lsty_dual iProto_dual_end=> /=. apply lsty_le_refl. Qed.
-
-  Lemma lsty_le_dual_end_r : ⊢ END <s: (lsty_dual (Σ:=Σ) END).
-  Proof. rewrite /lsty_dual iProto_dual_end=> /=. apply lsty_le_refl. 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_dual_message_l a A S :
+    ⊢ lsty_dual (lsty_message a A S) <s: lsty_message (action_dual a) A (lsty_dual S).
+  Proof.
+    iIntros "!>". rewrite /lsty_dual iProto_dual_message_tele. iApply iProto_le_refl.
+  Qed.
+  Lemma lsty_le_dual_message_r a A S :
+    ⊢ lsty_message (action_dual a) A (lsty_dual S) <s: lsty_dual (lsty_message a A S).
+  Proof.
+    iIntros "!>". rewrite /lsty_dual iProto_dual_message_tele. iApply iProto_le_refl.
+  Qed.
+  Lemma lsty_le_dual_send_l A S : ⊢ lsty_dual (<!!> A; S) <s: (<??> A; lsty_dual S).
+  Proof. apply lsty_le_dual_message_l. Qed.
+  Lemma lsty_le_dual_send_r A S : ⊢ (<!!> A; lsty_dual S) <s: lsty_dual (<??> A; S).
+  Proof. apply: lsty_le_dual_message_r. Qed.
+  Lemma lsty_le_dual_recv_l A S : ⊢ lsty_dual (<??> A; S) <s: (<!!> A; lsty_dual S).
+  Proof. apply lsty_le_dual_message_l. Qed.
+  Lemma lsty_le_dual_recv_r A S : ⊢ (<??> A; lsty_dual S) <s: lsty_dual (<!!> A; S).
+  Proof. apply: lsty_le_dual_message_r. Qed.
+
+  Lemma lsty_le_dual_end_l : ⊢ lsty_dual (Σ:=Σ) END <s: END.
+  Proof. rewrite /lsty_dual iProto_dual_end=> /=. apply lsty_le_refl. Qed.
+  Lemma lsty_le_dual_end_r : ⊢ END <s: lsty_dual (Σ:=Σ) END.
+  Proof. rewrite /lsty_dual iProto_dual_end=> /=. apply lsty_le_refl. Qed.
+
   Lemma lsty_le_rec_1 (C : lsty Σ → lsty Σ) `{!Contractive C} :
     ⊢ lsty_rec C <s: C (lsty_rec C).
   Proof.