proposition: Lemma interp_well_defined_2 : forall R1 R2 f2 l, Interp_dom R1 R2 (Term f2 l) -> defined R2 f2 -> forall (t : term), one_step (@union _ R1 R2) t (Term f2 l) -> Interp_dom R1 R2 t.
proof: Proof. intros R1 R2 f2 l H Df2 t t_R_f2l p f k Sub _. apply acc_subterms_3 with p t; trivial. apply Acc_inv with (Term f2 l); trivial. apply H with (@nil nat); trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)