test-suite/bugs/opened/4214.v


1
2
3
4
5

(* Check that subst uses all equations around *)
Goal forall A (a b c : A), b = a -> b = c -> a = c.
intros.
subst.
Fail reflexivity.