blob: f73c627ee4594091c303a1eeab2d30c7af6522b0 (
plain)
1
2
3
4
5
6
7
8
9
10
|
Set Primitive Projections.
Record Pack (A : Type) := pack { unpack : A }.
Definition p : Pack bool.
Proof.
refine (pack _ true).
Qed.
Definition boom : unpack bool p = let u := unpack _ in u p := eq_refl.
|