proposition: Theorem Hindley_Rosen_union A: forall (a b c : X A A), c#*a# <== a#*c# -> c#*b# <== b#*c# -> c#*(a+b)# <== (a+b)#*c#.
proof: Proof. intros a b c Ha Hb. do 2 rewrite (star_plus_star a b) at 1. apply semicomm_iter_right. semiring_normalize. auto with compat. Qed.
imports: ATBR(ATBR)