proposition: Lemma eval_erase_feval: forall n m a, eval n m (erase a) (feval a).
proof: Proof. induction a; constructor; trivial. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)