proposition: Theorem uniform_confluence : uniform_confluent step.
proof: Proof. Proof with repeat inv_step; eauto using step. intros s; induction s; intros t1 t2 step_s_t1 step_s_t2; try now inv step_s_t2. inv step_s_t1. - inv step_s_t2; try eauto; inv_step. - inv step_s_t2... + destruct (IHs2 _ _ H2 H3). * left. congruence. * right. destruct H as [u [A B]]... + right... - inv step_s_t2... + right... + destruct (IHs1 _ _ H2 H3). * left. congruence. * right. destruct H as [u [A B]]... Qed.
imports: Lia