proposition: Lemma confluence : confluent step.
proof: Proof. intros x y z x_to_y x_to_z. eapply star_pow in x_to_y. destruct x_to_y as [n x_to_y]. eapply star_pow in x_to_z. destruct x_to_z as [m x_to_z]. destruct (parametrized_confluence uniform_confluence x_to_y x_to_z) as [k [l [u [_ [_ [C [D _]]]]]]]. exists u. split; eapply star_pow; eexists; eassumption. Qed.
imports: Lia