proposition: Lemma rwr_interp_subst : forall sigma, forall t, Interp_dom (apply_subst sigma t) -> forall tsigma' sigma', Interp (apply_subst sigma t) tsigma' -> (forall x, In x (var_list t) -> Interp (apply_subst sigma (Var x)) (apply_subst sigma' (Var x))) -> (refl_trans_clos (one_step (Pi pi V0 V1)) (apply_subst sigma' t) tsigma' /\ match t with | Var _ => True | Term f l => ~G f -> match tsigma' with | Var _ => False | Term g k => f = g /\ refl_trans_clos (one_step_list (one_step (Pi pi V0 V1))) (map (apply_subst sigma') l) k end end).
proof: Proof. intros sigma t; pattern t; apply term_rec3; clear t. intros v Acc_t tsigma' sigma' I1 I2. assert (Acc_t' := interp_well_defined _ Acc_t). rewrite <- (interp_unicity _ Acc_t' _ _ I1 (I2 v (or_introl _ (eq_refl _)))); split; [left | exact I]. intros f l IHl Acc_t tsigma' sigma' I1 I2. assert (IHl' : forall t : term, In t l -> forall (tsigma' : term) (sigma' : substitution), Interp (apply_subst sigma t) tsigma' -> (forall x : variable, In x (var_list t) -> Interp (apply_subst sigma (Var x)) (apply_subst sigma' (Var x))) -> refl_trans_clos (one_step (Pi pi V0 V1)) (apply_subst sigma' t) tsigma'). intros s s_in_l ssigma'' sigma'' Issigma Isigma''. assert (Acc_ssigma : Interp_dom (apply_subst sigma s)). destruct (In_split _ _ s_in_l) as [l1 [l2 H3]]. apply interp_dom_subterm with (apply_subst sigma (Term f l)) (length l1 :: nil); trivial. subst l; simpl; rewrite map_app. rewrite <- (map_length (apply_subst sigma) l1); simpl. rewrite nth_error_at_pos; apply eq_refl. apply (proj1 (IHl s s_in_l Acc_ssigma ssigma'' sigma'' Issigma Isigma'')). inversion I1 as [ | f1 l1 l1' ll1 Cf1 Hl1 Hl1' Hll1 | f1 l1 l1' ll1 k1 kk1 Df1 Hl1 Hl1' Hll1 Hk1 Hk1' Hkk1]; clear I1; subst. assert (H0 : refl_trans_clos (one_step_list (one_step (Pi pi V0 V1))) (map (apply_subst sigma') l) (map (fun st : term * term => snd st) ll1)). clear IHl Acc_t; revert ll1 Hl1 Hll1 IHl'. induction l as [ | a l]; intros ll1 Hl1 Hll1 IH. destruct ll1; [left | discriminate Hl1]. destruct ll1 as [ | [a' a1] ll1]; [discriminate Hl1 | injection Hl1; clear Hl1; intros; subst]. simpl; rewrite refl_trans_clos_one_step_list_head_tail; split. apply IH; trivial. left; apply eq_refl. apply Hll1; left; apply eq_refl. intros; apply I2; simpl; apply in_or_app; left; assumption. apply IHl; trivial. intros; apply I2; simpl; apply in_or_app; right; assumption. intros; apply Hll1; right; trivial. apply (tail_prop _ IH). inversion H0 as [k | k1 k2 K]. split. left. intros _; split. apply eq_refl. left. split. right; apply general_context; assumption. intros _; split. apply eq_refl. right; assumption. split; [idtac | intro f_not_in_G; absurd (G f); assumption]. apply refl_trans_clos_is_trans with (Term f (map (fun st : term * term => snd st) ll1)). assert (refl_trans_clos (one_step_list (one_step (Pi pi V0 V1))) (map (apply_subst sigma') l) (map (fun st : term * term => snd st) ll1)). clear IHl Acc_t; revert ll1 Hl1 Hll1 IHl'; clear -I2. induction l as [ | a l]; intros ll1 Hl1 Hll1 IH. destruct ll1; [left | discriminate Hl1]. destruct ll1 as [ | [a' a1] ll1]; [discriminate Hl1 | injection Hl1; clear Hl1; intros; subst]. simpl; rewrite refl_trans_clos_one_step_list_head_tail; split. apply IH; trivial. left; apply eq_refl. apply Hll1; left; apply eq_refl. intros; apply I2; simpl; apply in_or_app; left; assumption. apply IHl; trivial. intros; apply I2; simpl; apply in_or_app; right; assumption. intros; apply Hll1; right; trivial. apply (tail_prop _ IH). simpl; destruct H as [k | k1 k2 H0]. left. right; apply general_context; assumption. right; apply project_comb; left; 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)