aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/5281.v
blob: 03bafdc9ae35ab84604e46e14150513a41d4029a (plain)
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.