proposition: Theorem SemiConfluence_is_WeakConfluence A: forall (a b : X A A), b * a# <== a# * b# <-> b# * a# <== a# * b#.
proof: Proof. intros a b; split. apply wsemicomm_iter_left. intro H. rewrite <- H. kleene_reflexivity. Qed.
imports: ATBR(ATBR)