[Agda] Proving equality of pairs

[David Leduc]

Hi,

Newbie's question again. Sorry!

How would you prove the simple lemma below?
Is it already in the standard library?
Why the first comma becomes yellow when I load the file?


module test where

open import Relation.Binary.PropositionalEquality
open import Data.Product

product-congr :
  (A B : Set)(x1 x2 : A)(y1 y2 : B) ->
  x1 ≡ x2 -> y1 ≡ y2 -> (x1 , y1) ≡ (x2 , y2)
product-congr A B x1 x2 y1 y2 = λ p q → {!!}