[Agda] Proving equality of pairs

[Nils Anders Danielsson]

On 2010-09-24 06:01, David Leduc wrote:
> 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?

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

product-congr :
   {A B : Set} {x1 x2 : A} {y1 y2 : B} →
   x1 ≡ x2 → y1 ≡ y2 → (x1 ,′ y1) ≡ (x2 , y2)
product-congr = P.cong₂ _,_

--
/NAD