From 6fe6a5635718fc1b86fb5f1757c3d0efdbd3bf89 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E6=9D=BE=E4=B8=8B=E7=A5=90=E4=BB=8B?= <y.skm24t@gmail.com>
Date: Fri, 18 Mar 2022 21:06:31 +0900
Subject: [PATCH] Minor fix
---
theories/typing/lib/smallvec/smallvec_push.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/typing/lib/smallvec/smallvec_push.v b/theories/typing/lib/smallvec/smallvec_push.v
index e1981f5f..06f1a12d 100644
--- a/theories/typing/lib/smallvec/smallvec_push.v
+++ b/theories/typing/lib/smallvec/smallvec_push.v
@@ -103,7 +103,7 @@ Section smallvec_push.
Lemma smallvec_push_type {𝔄} n (ty: type 𝔄) :
typed_val (smallvec_push n ty) (fn<α>(∅; &uniq{α} (smallvec n ty), ty) → ())
(λ post '-[(al, al'); a], al' = al ++ [a] → post ()).
-Proof.
+ Proof.
eapply type_fn; [apply _|]=> α ??[v[x[]]]. simpl_subst.
iIntros (?(pπ & bπ &[])?) "#LFT #TIME #PROPH #UNIQ #E Na L C /=(v & x &_) #Obs".
rewrite !tctx_hasty_val. iDestruct "v" as ([|dv]) "[_ v]"=>//.
--
GitLab