Skip to content
Snippets Groups Projects
Commit 6fe6a563 authored by Yusuke Matsushita's avatar Yusuke Matsushita
Browse files

Minor fix

parent 76b67715
Branches
Tags
No related merge requests found
Pipeline #63519 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/typing/lib/smallvec/smallvec_push.v
+ 1
− 1
View file @ 6fe6a563
...@@ -103,7 +103,7 @@ Section smallvec_push. ...@@ -103,7 +103,7 @@ Section smallvec_push.
Lemma smallvec_push_type {𝔄} n (ty: type 𝔄) : Lemma smallvec_push_type {𝔄} n (ty: type 𝔄) :
typed_val (smallvec_push n ty) (fn<α>(∅; &uniq{α} (smallvec n ty), ty) → ()) typed_val (smallvec_push n ty) (fn<α>(∅; &uniq{α} (smallvec n ty), ty) → ())
(λ post '-[(al, al'); a], al' = al ++ [a] → post ()). (λ post '-[(al, al'); a], al' = al ++ [a] → post ()).
Proof. Proof.
eapply type_fn; [apply _|]=> α ??[v[x[]]]. simpl_subst. eapply type_fn; [apply _|]=> α ??[v[x[]]]. simpl_subst.
iIntros (?(pπ & bπ &[])?) "#LFT #TIME #PROPH #UNIQ #E Na L C /=(v & x &_) #Obs". iIntros (?(pπ & bπ &[])?) "#LFT #TIME #PROPH #UNIQ #E Na L C /=(v & x &_) #Obs".
rewrite !tctx_hasty_val. iDestruct "v" as ([|dv]) "[_ v]"=>//. rewrite !tctx_hasty_val. iDestruct "v" as ([|dv]) "[_ v]"=>//.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment