A question from a groupchat

Intersperse.agda

{-# OPTIONS --cubical #-}

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

variable
  A : Type
  B : Type
  n : ℕ

insVec : A → List A → List A
insVec a [] = []
insVec a (x ∷ xs) = a ∷ x ∷ insVec a xs

dropHead : List A → List A
dropHead [] = []
dropHead (x ∷ xs) = xs

intersperse : A → List A → List A
intersperse a xs = dropHead (insVec a xs)

lem : {f : A → B} {a : A} (xs : List A) →
  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 : List A) →
  map f (intersperse a xs) ≡ intersperse (f a) (map f xs)
thm [] = refl
thm (x ∷ xs) = ap (_ ∷_) (lem xs)