proposition: Lemma sequal_clean_zero_equiv x : sequal (clean x) zero -> is_zero (clean x) = true.
proof: Proof. intros; rewrite <- (Clean.rewrite_idem x). apply sequal_equal in H. rewrite (Clean.equal_rewrite_zero_equiv H). reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)