test-suite/bugs/closed/5697.v


1
2
3
4
5
6
7
8
9
10

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.