proposition: Lemma clean0_idem: forall x, clean0 (clean0 x) = clean0 x.
proof: Proof. intro x; induction x; trivial; simpl. destruct_tests; trivial. simpl. rewrite IHx1, IHx2. destruct_tests; reflexivity. destruct_tests; trivial. simpl. rewrite IHx1, IHx2. destruct_tests; reflexivity. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)