Skip to content
Snippets Groups Projects
Commit 75f6aaae authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Nit.

parent b6389b47
Branches
Tags
No related merge requests found
Pipeline #46129 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 1 deletion
theories/typing/sum.v
+ 2
− 1
View file @ 75f6aaae
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.algebra Require Import list. From iris.algebra Require Import list.
From iris.bi Require Import fractional. From iris.bi Require Import fractional.
From lrust.typing Require Import lft_contexts.
From lrust.typing Require Export type. From lrust.typing Require Export type.
Set Default Proof Using "Type". Set Default Proof Using "Type".
...@@ -126,7 +127,7 @@ Section sum. ...@@ -126,7 +127,7 @@ Section sum.
Proper (Forall2 (subtype E L) ==> subtype E L) sum. Proper (Forall2 (subtype E L) ==> subtype E L) sum.
Proof. Proof.
iIntros (tyl1 tyl2 Htyl qmax qL) "HL". iIntros (tyl1 tyl2 Htyl qmax qL) "HL".
iAssert (□ (lft_contexts.elctx_interp E -∗ ⌜max_list_with ty_size tyl1 = max_list_with ty_size tyl2⌝))%I with "[#]" as "#Hleq". iAssert (□ (elctx_interp E -∗ ⌜max_list_with ty_size tyl1 = max_list_with ty_size tyl2⌝))%I with "[#]" as "#Hleq".
{ iInduction Htyl as [|???? Hsub] "IH". { iInduction Htyl as [|???? Hsub] "IH".
{ iClear "∗". iIntros "!# _". done. } { iClear "∗". iIntros "!# _". done. }
iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH". iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH".
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment