module exampleProductElim where

record _×_  (A B : Set) : Set where 
  field
     first  : A
     second : B

postulate A : Set
postulate B : Set
postulate C : Set


f : (A -> B × C) -> A -> B
f = \(a-bc : A -> B × C) 
     -> \(a : A) 
     -> let 
          bc : B × C
          bc = a-bc a
        in  _×_.first bc


f' : (A -> B × C) -> A -> B
f' = \(a-bc : A -> B × C) 
     -> \(a : A) 
     -> _×_.first (a-bc a)