proposition: Theorem equal_to_sequal : forall x y, equal x y -> sequal (clean x) (clean y).
proof: Proof. intros; induction H; cbn in *; trivial; destruct_tests; simpl; trivial; try solve [ constructor; rewrite ? Clean.rewrite_idem; trivial | match goal with H: sequal (clean _) zero |- _ => rewrite (sequal_clean_zero_equiv H) in *; discriminate end | match goal with H: sequal zero (clean _) |- _ => rewrite (sequal_clean_zero_equiv (sequal_sym H)) in *; discriminate end | econstructor; eauto ]. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)