proposition: Lemma In_reducts2_vec_intro : forall n (ts : terms n) t i (p : i < n), In t (reducts2 (Vnth ts p)) -> In (Vreplace ts p t) (reducts2_vec ts).
proof: Proof. induction ts. intros. lia. destruct i; simpl; intro; rewrite in_app. left. apply in_map with (f := fun x => Vcons x ts). hyp. right. apply in_map with (f := fun x => Vcons h x). apply IHts. hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)