module Test2 where

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

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