proposition: Lemma clean_correct: forall x, equal x (clean1 (clean0 x)).
proof: Proof. intro. rewrite <- clean1_correct. apply clean0_correct. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)