proposition: Lemma decide_typed: forall n m (a b: Semiring.X n m), decide (erase a) (erase b) = true -> feval a == feval b.
proof: Proof. intros. apply erase_faithful, decide_correct. assumption. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)