proposition: Lemma R1_at_top_aux_1 : forall t sigma sigma', (forall f, symb_in_term f t = true -> ~defined R2 f) -> Interp_dom R1 R2 (apply_subst sigma t) -> Interp_subst (var_list t) sigma sigma' -> Interp (apply_subst sigma t) (apply_subst sigma' t).
proof: Proof. intro t; pattern t; apply term_rec3; clear t. intros v sigma sigma' _ Ht Hsigma; apply (proj2 (Hsigma v (or_introl _ (eq_refl _)))). intros f l IH sigma sigma' Ct Ht Hsigma; simpl. apply (Ccase f (map (apply_subst sigma) l) (map (apply_subst sigma') l) (map (fun t => (apply_subst sigma t, apply_subst sigma' t)) l)). simpl; apply Ct; rewrite symb_in_term_unfold. generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _; trivial | intros f_diff_f; absurd (f = f); trivial]. rewrite map_map; simpl; trivial. rewrite map_map; simpl; trivial. intros s s'; rewrite in_map_iff; intros [u [H' u_in_l]]. injection H'; intros; subst; clear H'. assert (Cu : forall f0, symb_in_term f0 u = true -> ~ defined R2 f0). intros g Hg; apply Ct. rewrite symb_in_term_unfold. generalize (F.Symb.eq_bool_ok g f); case (F.Symb.eq_bool g f); [intros g_eq_f | intros g_diff_f]; trivial. simpl; destruct (In_split _ _ u_in_l) as [l' [l'' H1]]; subst l. rewrite symb_in_term_list_app. destruct (symb_in_term_list g l'); simpl; trivial. rewrite Hg; simpl; trivial. assert (Hu : Interp_dom R1 R2 (apply_subst sigma u)). simpl in Ht; apply (interp_well_defined_1 R1 R2 _ _ Ht). rewrite in_map_iff. exists u; split; trivial. apply (IH u u_in_l sigma sigma' Cu Hu). intros v v_in_u; apply (Hsigma v). rewrite var_list_unfold. generalize l u_in_l; intro k; induction k as [ | t k]. contradiction. intros [u_eq_t | u_in_k]. subst; simpl; apply in_or_app; left; trivial. simpl; apply in_or_app; right; apply IHk; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)