proposition: Lemma R1_at_top : forall S1, @inclusion _ S1 R1 -> forall l r, S1 r l -> forall sigma, Interp_dom R1 R2 (apply_subst sigma l)-> {sigma' : substitution & {s' : term & {t' : term | Interp_subst (var_list l) sigma sigma' /\ Interp (apply_subst sigma l) s' /\ Interp (apply_subst sigma r) t' /\ axiom S1 t' s'} } }.
proof: Proof. inversion module_R1_R2 as [M]. intros S1 S1_in_R1 l r r_R1_l sigma Hl. assert (Cl : forall f, symb_in_term f l = true -> ~defined R2 f). intros f f_in_l Df; generalize (M f r l Df (S1_in_R1 _ _ r_R1_l)). replace (r :: l :: nil) with ((r :: nil) ++ (l :: nil)); trivial. rewrite symb_in_term_list_app. simpl; rewrite f_in_l. destruct (symb_in_term f r); simpl; discriminate. assert (Cr : forall f, symb_in_term f r = true -> ~defined R2 f). intros f f_in_r Df; generalize (M f r l Df (S1_in_R1 _ _ r_R1_l)). replace (r :: l :: nil) with ((r :: nil) ++ (l :: nil)); trivial. rewrite symb_in_term_list_app; simpl. rewrite f_in_r; simpl; discriminate. destruct (R1_at_top_aux_2 l Cl sigma Hl) as [sigma' Hsigma]. exists sigma'. destruct (interp_defined _ Hl) as [s' Hs']; exists s'. assert (Hsigma' : Interp_subst (var_list r) sigma sigma'). intros v v_in_r; apply (Hsigma v). apply R1_reg with r; trivial; apply S1_in_R1; trivial. assert (Hr : Interp_dom R1 R2 (apply_subst sigma r)). refine (interp_dom_R1 R1 R2 _ _ _ _ _ _ Hl _); trivial. apply at_top; apply instance; apply S1_in_R1; trivial. destruct (interp_defined _ Hr) as [t' Ht']; exists t'. split; trivial. split; trivial. split; trivial. assert (Hs'' := R1_at_top_aux_1 l sigma sigma' Cl Hl Hsigma). rewrite (interp_unicity _ Hl _ _ Hs' Hs''). assert (Ht'' := R1_at_top_aux_1 r sigma sigma' Cr Hr Hsigma'). rewrite (interp_unicity _ Hr _ _ Ht' Ht''). apply instance; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)