diff --git a/theories/typing/lib/smallvec/smallvec_push.v b/theories/typing/lib/smallvec/smallvec_push.v
index e1981f5f142659ccda592f12b57d98156be5aa0c..06f1a12de5707b5661aa2a1c4321fe41bddb389e 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]"=>//.