proposition: Lemma In_subterm_lst_vec_elim : forall v n (ts : terms n), In v (subterm_lst_vec ts) -> exists i, exists p : i < n, In v (subterm_lst (Vnth ts p)).
proof: Proof. induction ts. contr. intros In_v; simpl in In_v. rewrite in_app in In_v. intuition. exists 0. exists (Nat.lt_0_succ n). simpl. hyp. destruct H0 as [i H0]. destruct H0 as [p H0]. assert (p' : S i < S n). lia. exists (S i). exists p'. simpl. assert (H1 : (NatCompat.lt_S_n p') = p). apply lt_unique. rewrite H1. hyp. Qed.
imports: CoLoR(AContext VecUtil ListUtil LogicUtil NatUtil RelUtil ASN)