proposition: Lemma equal_clean_zero_equiv : forall x y, equal x y -> is_zero (clean0 x) = is_zero (clean0 y).
proof: Proof. intros; induction H; simpl; destruct_tests; reflexivity. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)