module Test where

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

pairing : ∀ {A : Set} {P : A → Set} (p : ∃ P) → < proj₁ , proj₂ > p ≡ p
pairing (x , y) = refl