blob: 3d30b62f80c138769cd925ad8fa56ff56e250504 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
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.
refine (f_equal _ _).
Undo.
apply f_equal.
admit.
Qed.
|