proposition: Lemma confluence : forall x, confluence _ (Eqt.one_step R) x.
proof: Proof. apply Newman. exact wf_R. intros x. induction x using term_rec4 with (Pl:=fun lx => local_confluence _ (one_step_list (one_step R)) lx). intros y z H H0. inversion H; clear H;subst. apply no_need_of_instance in H1. elim (R_non_var _ _ H1). intros y z Hy Hz. inversion Hy;subst. apply no_need_of_instance in H. apply head_down_confl with (1:=Hz) (2:=H). inversion Hz;clear Hz;subst. apply no_need_of_instance in H. apply coherence_sym. apply head_down_confl with (1:=Hy) (2:=H). destruct (IHx _ _ H1 H2) as [lz [Hlz1 Hlz2]]. exists (Term f lz);split. apply star_list;assumption. apply star_list;assumption. revert H;induction l. intros;red;intros;inversion H0. intros;red;intros. inversion H0;inversion H1;clear H0 H1;subst. assert (coherence _ (one_step R) t0 t1). apply H with a;simpl;auto. destruct H0 as [t [h1 h2]]. exists (t::l);split;apply star_cons; try constructor;auto. exists (t1::l1);split;auto using star_cons; apply star_R;constructor;auto. exists (t1::l1);split;auto using star_cons; apply star_R;constructor;auto. assert (coherence _ (one_step_list (one_step R)) l1 l0). apply IHl;simpl in H;auto. destruct H0 as [lz [h1 h2]]. exists (a::lz);split;apply star_cons;auto;constructor. Qed.
imports: CoLoR(weaved_relation closure terminaison) CoLoR(equational_theory_spec)