proposition: Lemma acc_interp_dom : forall t, Acc (one_step (@union _ R1 R2)) t -> Interp_dom R1 R2 t.
proof: Proof. intros t Acc_t p f l Sub _. apply acc_subterms_3 with p t; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)