Proof of equivalence of two similar zip implementations

ziplist.agda

open import Agda.Builtin.Equality

record _∧_ (A B : Set) : Set where
  constructor conj
  field
    proj₁ : A
    proj₂ : B

data List (A : Set) : Set where
  ⊥ : List A
  nil : List A
  _∷_ : A → List A → List A

eq-lemma : {A : Set} {a a₁ : A} {ℓ ℓ₁ : List A} → a ≡ a₁ → ℓ ≡ ℓ₁ → (a ∷ ℓ) ≡ (a₁ ∷ ℓ₁)
eq-lemma refl refl = refl

zip₁ : {A B : Set} → List A → List B → List (A ∧ B)
zip₁ ⊥ _ = ⊥
zip₁ nil _ = nil
zip₁ _ ⊥ = ⊥
zip₁ _ nil = nil
zip₁ (x ∷ xs) (y ∷ ys) = conj x y ∷ zip₁ xs ys

zip₂ : {A B : Set} → List A → List B → List (A ∧ B)
zip₂ ⊥ _ = ⊥
zip₂ (x ∷ xs) ⊥ = ⊥
zip₂ (x ∷ xs) (y ∷ ys) = conj x y ∷ zip₂ xs ys
zip₂ _ _ = nil

zip-proof : {A B : Set} (ℓ₁ : List A) (ℓ₂ : List B) → zip₁ ℓ₁ ℓ₂ ≡ zip₂ ℓ₁ ℓ₂
zip-proof ⊥ _ = refl
zip-proof nil _ = refl
zip-proof (x ∷ ℓ₁) ⊥ = refl
zip-proof (x ∷ ℓ₁) nil = refl
zip-proof (x ∷ ℓ₁) (x₁ ∷ ℓ₂) with zip-proof ℓ₁ ℓ₂
zip-proof (x ∷ ℓ₁) (x₁ ∷ ℓ₂) | cc = eq-lemma refl cc