proposition: Theorem equal_eval: forall x' y', RegExp.equal x' y'-> forall A B x y, eval A B x' x -> eval A B y' y -> x==y.
proof: Proof. intros x' y' H A B x y Hx Hy. destruct (eval_clean Hx) as [x1 Hx1 Hx1']. destruct (eval_clean Hy) as [y1 Hy1 Hy1']. destruct (eval_sequal (equal_to_sequal H) Hx1) as [y2 Hy2 Hy2']. rewrite Hx1', Hy1', Hy2'. rewrite (eval_inj Hy2 Hy1). reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)