proposition: Lemma var_in_replace_at_pos : forall s p u x, In x (var_list (replace_at_pos s u p)) -> In x (var_list s) \/ In x (var_list u).
proof: Proof. intros s p; revert s; induction p as [ | i p]. simpl; intros s u x x_in_u; right; assumption. intros s u x; destruct s as [v | f l]. left; trivial. rewrite replace_at_pos_unfold; do 2 rewrite var_list_unfold. clear f; revert i u x; induction l as [ | t l]; intros i u x. contradiction. simpl replace_at_pos_list; destruct i as [ | i]. simpl; intro H; destruct (in_app_or _ _ _ H) as [H1 | H1]; clear H. destruct (IHp _ _ _ H1) as [H2 | H2]; clear H1. left; apply in_or_app; left; assumption. right; assumption. left; apply in_or_app; right; assumption. simpl; intro H; destruct (in_app_or _ _ _ H) as [H1 | H1]; clear H. left; apply in_or_app; left; assumption. destruct (IHl _ _ _ H1) as [H2 | H2]; clear H1. left; apply in_or_app; right; assumption. right; assumption. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)