proposition: Lemma interp_dom_subst : forall R1 R2 t sigma, Interp_dom R1 R2 (apply_subst sigma t) -> forall v, In v (var_list t) -> Interp_dom R1 R2 (apply_subst sigma (Var v)).
proof: Proof. intros R1 R2 t sigma Itsigma v v_in_t. destruct (var_in_subterm2 v t) as [p H]. apply in_impl_mem; trivial. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos t p sigma). rewrite H. apply interp_dom_subterm; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)