proposition: Lemma in_vars_subterm : forall x t, In x (vars t) -> exists ps, subterm_pos t ps = Some (Var x).
proof: Proof. intros x t; pattern t; apply term_ind with (Q := fun n (ts : terms n) => In x (vars_vec ts) -> exists i, exists h:i<n, exists ps, subterm_pos (Vnth ts h) ps = Some (Var x)); clear t. intro y. simpl. intuition. subst. exists nil. refl. intros f ts IH h. rewrite vars_fun in h. destruct (IH h). do 2 destruct H. exists (x0::x2). simpl. case (lt_ge_dec x0 (arity f)); intro. rewrite (lt_unique l x1). hyp. lia. simpl. tauto. intros t n ts ht hts. simpl vars_vec. rewrite in_app. intros [h|h]. destruct (ht h). exists 0. exists (Nat.lt_0_succ n). exists x0. simpl. hyp. destruct (hts h). do 2 destruct H. exists (S x0). exists (NatCompat.lt_n_S x1). exists x2. simpl. rewrite (lt_unique (NatCompat.lt_S_n (NatCompat.lt_n_S x1)) x1). hyp. Qed.
imports: CoLoR(ATrs ListUtil NatUtil VecUtil LogicUtil OptUtil)