proposition: Theorem erase_faithful: forall n m (a b: Semiring.X n m), U.equal (erase a) (erase b) -> feval a == feval b.
proof: Proof. intros. eapply equal_eval; eauto using eval_erase_feval. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)