proposition: Lemma conv_star A (a: X A A): a# ` == a` #.
proof: Proof. apply leq_antisym. switch. rewrite <- (dot_neutral_right (a#)). apply star_destruct_left_old'. switch. rewrite <- star_make_left_c at 2. semiring_reflexivity. rewrite <- (dot_neutral_right (a`#)). apply star_destruct_left_old'. switch. rewrite <- star_make_left_c at 2. semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(SemiLattice) ATBR(SemiRing)