proposition: Theorem Hindley_Rosen_confluent_union A: forall (a b : X A A), a`#*a# <== a#*a`# -> b`#*b# <== b#*b`# -> a`#*b# <== b#*a`# -> (a+b)`#*(a+b)# <== (a+b)#*(a+b)`#.
proof: Proof. intros a b Ha Hb Hab. do 2 rewrite conv_plus at 1. do 2 rewrite (star_plus_star (b`) (a`)) at 1. apply semicomm_iter_left. semiring_normalize. rewrite 2 Hindley_Rosen_union; trivial with algebra. switch. assumption. Qed.
imports: ATBR(ATBR)