Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Inductive paths A (x : A) : A -> Type := idpath : paths A x x.
Notation "x = y" := (@paths _ x y) : type_scope.
Axioms A B : Type.
Axiom P : A = B.
Definition foo : (A = B) * (A = B).
split; abstract (rewrite <- P; reflexivity).
Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
There's another error that I get on the rewrite, sometimes, but I'm still working on a test case for that one.
There's another error that I get on the rewrite, sometimes, but I'm still working on a test case for that one.