proposition: Lemma R1_at_top_dp : forall S1, @inclusion _ S1 R1 -> forall l t r p, S1 t l -> subterm_at_pos t p = Some r -> forall sigma, Interp_dom R1 R2 (apply_subst sigma l)-> {sigma' : substitution | Interp_subst (var_list l) sigma sigma' /\ Interp_dom R1 R2 (apply_subst sigma r) /\ Interp (apply_subst sigma l) (apply_subst sigma' l) /\ Interp (apply_subst sigma r) (apply_subst sigma' r) }.
proof: Proof. inversion module_R1_R2 as [M]. intros S1 S1_in_R1 l t r p t_R1_l t_p_eq_r sigma Hl. assert (Cl : forall f, symb_in_term f l = true -> ~defined R2 f). intros f f_in_l Df; generalize (M f t l Df (S1_in_R1 _ _ t_R1_l)). replace (t :: l :: nil) with ((t :: nil) ++ (l :: nil)); trivial. rewrite symb_in_term_list_app. simpl; rewrite f_in_l. destruct (symb_in_term f t); simpl; discriminate. assert (Ct : forall f, symb_in_term f t = true -> ~defined R2 f). intros f f_in_t Df; generalize (M f t l Df (S1_in_R1 _ _ t_R1_l)). replace (t :: l :: nil) with ((t :: nil) ++ (l :: nil)); trivial. rewrite symb_in_term_list_app; simpl. rewrite f_in_t; simpl; discriminate. assert (Cr : forall f, symb_in_term f r = true -> ~defined R2 f). intros f f_in_r; apply Ct; apply symb_in_subterm with r p; trivial. destruct l as [v | f l]. absurd (R1 t (Var v)). apply R1_var. apply S1_in_R1; trivial. assert (Cf : ~defined R2 f). apply Cl; rewrite symb_in_term_unfold. simpl; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intros f_diff_f; absurd (f = f)]; trivial. assert (H' := R1_at_top _ S1_in_R1 _ _ t_R1_l sigma). destruct (R1_at_top_aux_2 (Term f l) Cl sigma Hl) as [sigma' Hsigma]. exists sigma'. assert (Hsigma' : Interp_subst (var_list t) sigma sigma'). intros v v_in_t; apply (Hsigma v); apply R1_reg with t; trivial; apply S1_in_R1; trivial. assert (Hsigma'' : Interp_subst (var_list r) sigma sigma'). intros v v_in_r; apply (Hsigma' v). apply var_in_subterm with r p; trivial. assert (Ht : Interp_dom R1 R2 (apply_subst sigma t)). refine (interp_dom_R1 _ _ _ _ _ _ _ _ Hl _); trivial. apply at_top; apply instance; apply S1_in_R1; trivial. assert (Hr : Interp_dom R1 R2 (apply_subst sigma r)). generalize t r t_p_eq_r Ht; clear t r t_p_eq_r Ht t_R1_l Ct Cr H' Hsigma' Hsigma''. induction p as [ | i p]; intros t r t_p_eq_r Ht. simpl in t_p_eq_r; injection t_p_eq_r; intro; subst; trivial. simpl in t_p_eq_r; destruct t as [ | g ll]. discriminate. assert (H' := nth_error_ok_in i ll). destruct (nth_error ll i) as [ti | ]. destruct (H' _ (eq_refl _)) as [l1 [l2 [L H'']]]; subst ll. apply (IHp ti r); trivial. simpl in Ht; apply (interp_well_defined_1 R1 R2 _ _ Ht). rewrite in_map_iff. exists ti; split; trivial. apply in_or_app; right; left; trivial. discriminate. split; trivial; split; trivial; split. exact (R1_at_top_aux_1 (Term f l) sigma sigma' Cl Hl Hsigma). destruct r as [v | g k]. apply (proj2 (Hsigma'' v (or_introl _ (eq_refl _)))). exact (R1_at_top_aux_1 (Term g k) sigma sigma' Cr Hr Hsigma''). Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)