fact: Definition Interp_subst lv sigma sigma' := forall v, In v lv -> Interp_dom R1 R2 (apply_subst sigma (Var v)) /\ Interp (apply_subst sigma (Var v)) (apply_subst sigma' (Var v)).
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)