proposition: Theorem WeakConfluence_is_ChurchRosser A: forall (a b : X A A), b# * a# <== a# * b# <-> (a+b)# <== a# * b#.
proof: Proof. intros a b; split; intro H. star_left_induction. semiring_normalize. rewrite (a_leq_star_a b) at 2. rewrite H. kleene_reflexivity. rewrite <- H. kleene_reflexivity. Qed.
imports: ATBR(ATBR)