blob: c653f992af4d34be64a82e5e272c3efb19078b8b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Set Primitive Projections.
Record foo : Type := Foo { foo_car: nat }.
Goal forall x y : nat, x <> y -> Foo x <> Foo y.
Proof.
intros.
intros H'.
congruence.
Qed.
Record bar (A : Type) : Type := Bar { bar_car: A }.
Goal forall x y : nat, x <> y -> Bar nat x <> Bar nat y.
Proof.
intros.
intros H'.
congruence.
Qed.
|
