proposition: Lemma occ_var_is_a_subterm_at_pos : forall x t, VSet.mem x (set_of_variables t) -> exists p, subterm_at_pos t p = Some (Var x).
proof: Proof. intros x t; pattern t; apply term_rec3; clear t. intros v; simpl; intros [x_eq_v | x_in_nil]; [idtac | contradiction]. exists (@nil nat); unfold VSet.LP.EDS.eq_A, VSet.EDS.eq_A , DecVar.eq_A in *; subst; trivial. intros f l IH x_in_l; assert (H : exists s, exists i, In s l /\ nth_error l i = Some s /\ VSet.mem x (set_of_variables s)). clear IH; simpl in x_in_l; induction l as [ | t l]; [contradiction | idtac]. destruct_set x_in_l x_in_t x_in_l'. exists t; exists 0; split; [left; trivial | split; trivial; simpl]. destruct (IHl x_in_l') as [s [i [s_in_l [s_eq_li x_in_s]]]]; exists s; exists (S i). split; [right; trivial | split; trivial]. destruct H as [s [i [s_in_l [s_eq_li x_in_s]]]]. destruct (IH s s_in_l x_in_s) as [p H]. exists (i :: p); simpl; rewrite s_eq_li; rewrite H; trivial. Qed.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)