proposition: Lemma idp_criterion : forall R, (forall x t, ~ (R t (Var x))) -> (forall s t, R s t -> forall x, In x (var_list s) -> In x (var_list t)) -> (forall f, {constructor R f} + {defined R f}) -> well_founded (idp_step R) -> well_founded (P_step R (inner R)).
proof: Proof. intros R HR RR CD Wf t; pattern t; apply term_rec3; clear t. intro x; apply Acc_intro; intros s H; inversion H; subst. inversion H1; subst. destruct t2 as [v2 | ]. absurd (R t1 (Var v2)); trivial; apply HR. discriminate. intros; apply idp_criterion_aux; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)