在Agda中，cong是一个用于证明等式的定理。它的类型是∀ {A : Set} {x y : A} {P : A → Set} → x ≡ y → P x → P y。

假设我们有一个类型为List ℕ的变量xs，我们想要证明map f (xs ++ ys) ≡ map f (ys ++ xs)，其中f : ℕ → ℕ是一个函数，ys是另一个List ℕ。

首先，我们需要定义map函数的类型和实现。这可以通过递归地定义来完成。以下是一个示例实现：

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

map : {A B : Set} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

接下来，我们可以使用cong来证明此等式。以下是一个示例证明的代码：

cong-append : {A : Set} {xs ys : List A} → (f : A → A) → map f (xs ++ ys) ≡ map f (ys ++ xs)
cong-append f = cong (λ xs → map f (xs ++ ys)) (map-append f xs ys) where
  xs : List A
  xs = xs
  
  ys : List A
  ys = ys

  map-append : {A B : Set} {xs ys : List A} → (f : A → B) → map f (xs ++ ys) ≡ map f xs ++ map f ys
  map-append f [] ys = refl
  map-append f (x ∷ xs) ys = cong (λ xs' → f x ∷ map f xs' ++ map f ys) (map-append f xs ys)

在上面的代码中，我们首先定义了一个辅助函数map-append，它证明了map函数的附加性质。然后，我们使用cong来证明等式map f (xs ++ ys) ≡ map f xs ++ map f ys，其中我们将map f (xs ++ ys)和map f (ys ++ xs)作为函数参数传递给cong。

最后，我们使用cong-append来证明map f (xs ++ ys) ≡ map f (ys ++ xs)，其中xs和ys是我们要附加的两个List ℕ。