proposition: Lemma clean0_correct: forall x, equal x (clean0 x).
proof: Proof. induction x; simpl; auto; destruct_tests; auto. rewrite IHx1; trivial. rewrite IHx2; trivial. rewrite IHx1, <- IHx2; trivial. rewrite <- IHx1, IHx2; trivial. rewrite plus_com; trivial. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)