proposition: Lemma sequal_equal x y: sequal x y -> equal x y .
proof: Proof. intros; induction H; solve [constructor; auto | eapply equal_trans; eauto]. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)