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.