proposition: Lemma In_subterm_lst_vec_intro : forall n (ts : terms n) v i (p : i < n), In v (subterm_lst (Vnth ts p)) -> In v (subterm_lst_vec ts).
proof: Proof. induction ts. intros. lia. destruct i; simpl; intros; rewrite in_app. left; hyp. right. apply (IHts _ _ (NatCompat.lt_S_n p)); auto. Qed.
imports: CoLoR(AContext VecUtil ListUtil LogicUtil NatUtil RelUtil ASN)