test-suite/bugs/opened/3625.v


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.