proposition: Lemma interp_well_defined_1 : forall R1 R2 f1 l, Interp_dom R1 R2 (Term f1 l) -> forall t, In t l -> Interp_dom R1 R2 t.
proof: Proof. intros R1 R2 f1 l H t t_in_l p f2 k H' Df2. destruct (In_split _ _ t_in_l) as [l' [l'' H'']]; subst l. apply (H ((length l') :: p)); trivial. simpl; rewrite nth_error_at_pos. trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)