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