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