proposition: Theorem erase_faithful: forall n m (a b: KA.X n m), RegExp.equal (erase a) (erase b) -> feval a == feval b.
proof: Proof. intros. eapply equal_eval; eauto using eval_erase_feval. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)