proposition: Lemma rewrite_idem: forall x, rewrite (rewrite x) = rewrite x.
proof: Proof. intro x; induction x; trivial; cbn; destruct_tests; trivial; simpl. rewrite IHx1, IHx2. destruct_tests. trivial. rewrite IHx1, IHx2. destruct_tests. trivial. rewrite IHx. destruct_tests. trivial. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)