blob: 868f45c89a46ad9515328d4d754fe67c3a9584ec (
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, fst x = fst y.
intros.
lazymatch goal with
| [ |- context[@fst ?A ?B] ] => pose (@fst A B) as fst';
progress change (@fst Set Set) with fst'
end.
Abort.
|
