A question from a groupchat

Intersperse.agda

{-# OPTIONS --cubical #-}

open import Cubical.Data.Vec
open import Cubical.Data.Nat.Base
open import Cubical.Data.Equality hiding (map)

variable
  A : Type
  B : Type
  n : ℕ

insVec : A → Vec A n → Vec A (doubleℕ n)
insVec a [] = []
insVec a (x ∷ xs) = a ∷ x ∷ insVec a xs

intersperse : A → Vec A n → Vec A (predℕ (doubleℕ n))
intersperse a [] = []
intersperse {n = n} a xs@(x ∷ _) = tail (insVec a xs)

lem : {f : A → B} {a : A} (xs : Vec A n) →
  map f (insVec a xs) ≡ insVec (f a) (map f xs)
lem [] = refl
lem {f = f} {a = a} (x ∷ xs) = ap (f a ∷_) (ap (_ ∷_) (lem xs))

thm : {f : A → B} {a : A} (xs : Vec A n) →
  map f (intersperse a xs) ≡ intersperse (f a) (map f xs)
thm [] = refl
thm (x ∷ xs) = ap (_ ∷_) (lem xs)