proposition: Lemma R_reg_one_step : forall t s, (one_step R) s t -> forall x, In x (var_list s) -> In x (var_list t).
proof: Proof. intro t; pattern t; apply term_rec3; clear t. intros v s H; inversion H as [t1 t2 H0 H1 H2 |]; clear H; subst. inversion H0 as [r l sigma H H1 H2]; clear H0; subst. destruct l as [x | ]; [idtac | discriminate]. apply False_rect; apply (R_var _ _ H). intros f l IHl s H; inversion H as [t1 t2 H0 H1 H2 | g l1 l2 H0 H1 H2]; clear H; subst. inversion H0 as [r l' sigma H H1 H2]. intros x x_in_left. destruct (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl a) _ _ x_in_left)) as [p Sub]. generalize (subterm_in_instantiated_term _ _ _ Sub). case_eq (subterm_at_pos r p); [intros u' Sub' | intro Sub']. destruct u' as [x' | ]; [idtac | intro; discriminate]. intro K; assert (x'_in_r : In x' (var_list r)). apply (var_in_subterm x' r p Sub'); left; reflexivity. assert (x'_in_l : In x' (var_list l')). apply (R_reg _ _ H); assumption. destruct (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl a) _ _ x'_in_l)) as [q Sub'']. apply var_in_subterm with (apply_subst sigma (Var x')) q. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos l' q sigma). rewrite Sub''; trivial. rewrite <- K; left; reflexivity. intros [x' [p' [p'' [K [x'_in_r [Sub1 Sub2]]]]]]. assert (x'_in_l : In x' (var_list l')). apply (R_reg _ _ H); assumption. destruct (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl a) _ _ x'_in_l)) as [q Sub'']. apply var_in_subterm with (apply_subst sigma (Var x')) q. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos l' q sigma). rewrite Sub''; trivial. apply var_in_subterm with (Var x) p''; trivial. left; reflexivity. destruct (one_step_in_list H0) as [t [s [k [k' [K [K1 K2]]]]]]; subst l l1. intro x; do 2 rewrite var_list_unfold; do 2 rewrite var_list_list_app. intro x_in_ksk'; destruct (in_app_or _ _ _ x_in_ksk') as [x_in_k | x_in_sk']. apply in_or_app; left; assumption. simpl in x_in_sk'; destruct (in_app_or _ _ _ x_in_sk') as [x_in_s | in_in_k']. apply in_or_app; right; apply in_or_app; left. apply IHl with s; trivial. apply in_or_app; right; left; reflexivity. apply in_or_app; right; simpl; apply in_or_app; right; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)