proposition: Lemma var_in_subterm : forall v s t p, subterm_at_pos t p = Some s -> In v (var_list s) -> In v (var_list t).
proof: Proof. intros v s t p; generalize s t; clear s t; induction p as [ | i p]; intros s t H v_in_s. simpl in H; injection H; clear H; intros; subst; trivial. simpl in H; destruct t as [ | g l]. discriminate. assert (H' := nth_error_ok_in i l). destruct (nth_error l i) as [ti | ]. destruct (H' _ (eq_refl _)) as [l1 [l2 [L H'']]]; subst l. rewrite var_list_unfold. clear H' L; induction l1 as [ | t1 l]. simpl; apply in_or_app; left; apply (IHp s ti); trivial. simpl; apply in_or_app; right; apply IHl. discriminate. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)