1 2 3 4 5 6 7
Set Implicit Arguments. Set Primitive Projections. Record prod A B := pair { fst : A ; snd : B }. Goal forall x y : prod Set Set, x.(@fst) = y.(@fst). intros. apply f_equal.