proposition: Theorem Newman : forall x:A, confluence x.
proof: Proof. intro x;pattern x. apply well_founded_ind with (1:=Hyp1). clear x;intros x IHx. red. intros y z Hy Hz. eapply Ind_proof with (1:=IHx);assumption. Qed.
imports: CoLoR(weaved_relation closure terminaison)