Issue323.agda

-- {-# OPTIONS -v tc.meta:20 #-}
-- Agdalist 2010-09-24 David Leduc
module Issue323 where

data Sigma (A : Set)(B : A -> Set) : Set where
  _,_ : (a : A) -> B a -> Sigma A B

data Trivial {A : Set}(a : A) : Set where
  trivial : Trivial a 

lemma : (A : Set)(x y : A) -> Trivial (x , y)
lemma A x y = trivial