test-suite/bugs/closed/2586.v


1
2
3
4
5
6

Require Import Setoid SetoidClass Program.

Goal forall `(Setoid nat) x y, x == y -> S x == S y.
  intros.
  Fail clsubst H0.
  Abort.