proposition: Lemma sequal_equal x y: sequal x y -> equal x y .
proof: Proof. intros; induction H; try solve [constructor; auto ]. eapply equal_trans; eauto. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(Reification)