proposition: Lemma interp_in_H : forall t, (forall g, symb_in_term g t = true -> ~G g) -> forall sigma sigma', (forall x, In x (var_list t) -> Interp (apply_subst sigma (Var x)) (apply_subst sigma' (Var x))) -> Interp (apply_subst sigma t) (apply_subst sigma' t).
proof: Proof. intros t; pattern t; apply term_rec3; clear t. intros v _ sigma sigma' Isigma; apply Isigma; left; apply eq_refl. intros f l IH fl_in_H sigma sigma' Isigma. simpl; constructor 2 with (map (fun t => (apply_subst sigma t, apply_subst sigma' t)) l). apply fl_in_H; simpl. rewrite eq_symb_bool_refl; apply eq_refl. rewrite map_map; simpl; apply eq_refl. rewrite map_map; simpl; apply eq_refl. intros s s' K; rewrite in_map_iff in K; destruct K as [t [K t_in_l]]; injection K; clear K; intros; subst. apply IH. assumption. intros g g_in_t; apply fl_in_H; apply symb_in_direct_subterm with t; trivial. intros x x_in_t; apply Isigma. destruct (In_split _ _ t_in_l) as [l1 [l2 K']]. apply var_in_subterm with t (length l1 :: nil); trivial. subst l; simpl; rewrite nth_error_at_pos; apply eq_refl. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)