proposition: Lemma technical_lemma : forall S1, @inclusion _ S1 R1 -> forall s s' t t', Interp_dom R1 R2 s -> Interp_dom R1 R2 t -> Interp s s' -> Interp t t' -> rdp_step (axiom (ddp S1)) (@union _ R1 R2) t s -> rdp_step (axiom (ddp S1)) (@union _ R1 (Pi pi V0 V1)) t' s'.
proof: Proof. inversion module_R1_R2 as [M]. intros S1 S1_in_R1 s s' t t' Is It Hs' Ht' t_R_s. inversion t_R_s as [f l1 l2 t'' l2_R_l1 H]; subst; clear t_R_s. assert (Is2 : Interp_dom R1 R2 (Term f l2)). assert (t2_R_t1 : refl_trans_clos (one_step (@union _ R1 R2)) (Term f l2) (Term f l1)). inversion l2_R_l1 as [l | l2' l1' l2_R_l1']; subst; [left | right; apply general_context; assumption]. inversion t2_R_t1 as [t12 | t2 t1 t2_R_t1']; clear t2_R_t1; subst. assumption. apply interp_dom_R1_R2_rwr with (Term f l1); assumption. destruct (interp_defined _ Is2) as [s'' Hs'']. inversion Hs' as [ | f' l' l'' ll1 Cf' Hl Hl' Hll1 | f' l' l'' ll1 Df Hl Hl' Hll1]; clear Hs'; subst. inversion Hs'' as [ | f'' k' k'' ll2 Cf'' Hk Hk' Hll2 | f'' k' k'' ll2 Df' Hk Hk' Hll2]; subst. apply (Rdp_step (axiom (ddp S1)) (@union term R1 (Pi pi V0 V1)) f (map (@snd _ _) ll1) (map (@snd _ _) ll2) t'); trivial. assert (Ill2 : forall s, In s (map (@fst _ _) ll2) -> Interp_dom R1 R2 s). intros; apply (interp_well_defined_1 R1 R2 _ _ Is2); trivial. assert (Ill1 : forall s, In s (map (@fst _ _) ll1) -> Interp_dom R1 R2 s). intros; apply (interp_well_defined_1 R1 R2 _ _ Is); trivial. clear Is H Is2 Hs''. revert ll1 Ill1 Ill2 Hll1 Hll2 l2_R_l1. induction ll2 as [ | [u u'] ll2]. intros [ | [v v'] ll1] Ill1 Ill2 Hll1 Hll2 l2_R_l1. left. generalize (refl_trans_clos_one_step_list_length_eq l2_R_l1); intros; discriminate. intros [ | [v v'] ll1]; simpl; intros Ill1 Ill2 Hll1 Hll2 l2_R_l1. generalize (refl_trans_clos_one_step_list_length_eq l2_R_l1); intros; discriminate. rewrite refl_trans_clos_one_step_list_head_tail; split. assert (u_R_v : refl_trans_clos (one_step (@union term R1 R2)) u v). apply refl_trans_clos_one_step_list_refl_trans_clos_one_step with nil (map (@fst _ _) ll2) nil (map (@fst _ _) ll1). apply eq_refl. assumption. inversion u_R_v as [uv | uu vv u_R_v']; clear u_R_v; subst. assert (Iv := Ill1 v (or_introl _ (eq_refl _))). rewrite (interp_unicity _ Iv v' u' (Hll1 _ _ (or_introl _ (eq_refl _))) (Hll2 _ _ (or_introl _ (eq_refl _)))). left. assert (Iv := Ill1 _ (or_introl _ (eq_refl _))). assert (Iu := Ill2 _ (or_introl _ (eq_refl _))). destruct (R1_R2_case _ _ Iv u_R_v') as [v'' [u'' [Iv' [Iu' H]]]]. rewrite (interp_unicity _ Iv _ _ (Hll1 _ _ (or_introl _ (eq_refl _))) Iv'). rewrite (interp_unicity _ Iu _ _ (Hll2 _ _ (or_introl _ (eq_refl _))) Iu'). right; assumption. apply (IHll2 ll1 (tail_prop _ Ill1) (tail_prop _ Ill2) (fun s s' H => Hll1 _ _ (or_intror _ H)) (fun s s' H => Hll2 _ _ (or_intror _ H))). rewrite refl_trans_clos_one_step_list_head_tail in l2_R_l1; apply (proj2 l2_R_l1). apply (technical_lemma_1 _ S1_in_R1 _ _ _ _ Is2 It Hs'' Ht' H). absurd (defined R2 f); trivial. absurd (defined R2 f); trivial. inversion H; clear H; subst. destruct t2 as [v2 | f2 k2]. destruct H2 as [H2 Sub]; inversion H2; clear H2; subst. absurd (R1 t2 (Var v2)). apply R1_var. apply S1_in_R1; trivial. destruct H2 as [H2 Sub]; inversion H2; clear H2; subst. injection H0; clear H0; intros; subst. intro D2f; generalize (M f _ _ D2f (S1_in_R1 _ _ H)). simpl; destruct (symb_in_term f t2); simpl. discriminate. rewrite eq_symb_bool_refl; discriminate. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)