test-suite/bugs/closed/5281.v


1
2
3
4
5
6

Inductive A (T : Prop) := B (_ : T).
Scheme Equality for A.

Goal forall (T:Prop), (forall x y : T, {x=y}+{x<>y}) -> forall x y : A T, {x=y}+{x<>y}.
decide equality.
Qed.