proposition: Lemma acc_one_step_interp_dom : forall t, Acc (one_step R) t -> Interp_dom t.
proof: Proof. intros t Acc_t; rewrite acc_with_subterm in Acc_t; induction Acc_t as [t Acc_t' IH]. assert (Acc_t : Acc (union term (one_step R) direct_subterm) t). apply Acc_intro; apply Acc_t'. clear Acc_t'. intros p f l K f_not_in_H. apply acc_subterms_3 with p t; trivial. rewrite acc_with_subterm; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)