proposition: Theorem equal_to_sequal : forall x y, equal x y -> sequal (clean0 x) (clean0 y).
proof: Proof. intros; induction H; simpl; trivial; destruct_tests; trivial; solve [ constructor; rewrite ? clean0_idem; trivial | rewrite (sequal_clean_zero_equiv IHequal1) in *; discriminate | rewrite (sequal_clean_zero_equiv IHequal2) in *; discriminate | rewrite (sequal_clean_zero_equiv (sequal_sym IHequal1)) in *; discriminate | rewrite (sequal_clean_zero_equiv (sequal_sym IHequal2)) in *; discriminate | econstructor; eauto ]. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)