4214.v « opened « bugs « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/bugs/opened/4214.v

blob: cd53c898e9f4b2b2295498b9f614916d546b8f0f (plain)

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