proposition: Lemma var_in_subterm2 : forall v t, mem (@eq _) v (var_list t) -> {p : list nat | subterm_at_pos t p = Some (Var v)}.
proof: Proof. intros v t; pattern t; apply term_rec3; clear t. intros x v_in_x; exists (@nil nat); simpl; destruct v_in_x as [v_eq_x | v_in_nil]; [subst; apply eq_refl | contradiction]. intros f l; rewrite var_list_unfold; simpl. induction l as [ | t l]; intros IH v_in_l. contradiction. simpl in v_in_l. generalize (mem_bool_ok _ _ X.eq_bool_ok v (var_list t)); case (mem_bool X.eq_bool v (var_list t)); [intro v_in_t | intro v_not_in_t]. destruct (IH t (or_introl _ (eq_refl _)) v_in_t) as [p Sub]. exists (0 :: p); simpl; trivial. assert (v_in_l' : mem (@eq _) v (var_list_list l)). rewrite <- mem_or_app in v_in_l; destruct v_in_l as [v_in_t | v_in_l]. absurd (mem (@eq _) v (var_list t)); trivial. assumption. destruct (IHl (tail_set _ IH) v_in_l') as [p Sub]; trivial. destruct p as [ | i p]; simpl in Sub. discriminate. exists (S(i) :: p); simpl; trivial. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)