From 2ae69856ed36d73bde10ca8a336323207aad786f Mon Sep 17 00:00:00 2001 From: jihgfee <jihgfee@gmail.com> Date: Wed, 22 Apr 2020 14:59:18 +0200 Subject: [PATCH] Clean up --- theories/logrel/subtyping.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v index 6fe8318..8da5498 100644 --- a/theories/logrel/subtyping.v +++ b/theories/logrel/subtyping.v @@ -56,9 +56,9 @@ Section subtype. Lemma lty_bi_le_refl A : ⊢ A <:> A. Proof. iSplit; iApply lty_le_refl. Qed. - Lemma lty_bi_le_trans A1 A2 A3 : ⊢ A1 <:> A2 -∗ A2 <:> A3 -∗ A1 <:> A3. + Lemma lty_bi_le_trans A1 A2 A3 : A1 <:> A2 -∗ A2 <:> A3 -∗ A1 <:> A3. Proof. iIntros "#[H11 H12] #[H21 H22]". iSplit; by iApply lty_le_trans. Qed. - Lemma lty_bi_le_sym A1 A2 : ⊢ A1 <:> A2 -∗ A2 <:> A1. + Lemma lty_bi_le_sym A1 A2 : A1 <:> A2 -∗ A2 <:> A1. Proof. iIntros "[$$]". Qed. Lemma lty_le_copy A : ⊢ copy A <: A. @@ -201,9 +201,9 @@ Section subtype. Lemma lsty_bi_le_refl S : ⊢ S <s:> S. Proof. iSplit; iApply lsty_le_refl. Qed. - Lemma lsty_bi_le_trans S1 S2 S3 : ⊢ S1 <s:> S2 -∗ S2 <s:> S3 -∗ S1 <s:> S3. + Lemma lsty_bi_le_trans S1 S2 S3 : S1 <s:> S2 -∗ S2 <s:> S3 -∗ S1 <s:> S3. Proof. iIntros "#[H11 H12] #[H21 H22]". iSplit; by iApply lsty_le_trans. Qed. - Lemma lsty_bi_le_sym S1 S2 : ⊢ S1 <s:> S2 -∗ S2 <s:> S1. + Lemma lsty_bi_le_sym S1 S2 : S1 <s:> S2 -∗ S2 <s:> S1. Proof. iIntros "[$$]". Qed. Lemma lsty_le_send A1 A2 S1 S2 : -- GitLab