blob: b4705780dbe1fc82f626edb71fbd1e73aa7f29f8 (
plain)
1
2
3
4
5
6
7
|
Set Primitive Projections.
Record prod A B := pair { fst : A ; snd : B }.
Goal forall A B (p : prod A B), p = let (x, y) := p in pair A B x y.
Proof.
intros A B p.
exact eq_refl.
Qed.
|