proposition: Theorem Hindley_Rosen A: forall (a b : X A A), b*a <== a#*(b+1) -> b#*a# <== a#*b#.
proof: Proof. intros. do 2 rewrite (star_plus_one b) at 1. apply semicomm_iter_left. rewrite <- (star_idem a) at 2. apply semicomm_iter_right. semiring_normalize. rewrite H. kleene_reflexivity. Qed.
imports: ATBR(ATBR)