proposition: Lemma In_reducts2_vec_elim : forall n (vs ts : terms n), In vs (reducts2_vec ts) -> exists i, exists p : i < n, exists u, In u (reducts2 (Vnth ts p)) /\ vs = Vreplace ts p u.
proof: Proof. induction ts; intros. contr. simpl in H. rewrite in_app in H. split_all; ded (in_map_elim H); clear H; decomp H0. set (p := Nat.lt_0_succ n). ex 0 p x. simpl. auto. ded (IHts x H1); clear IHts. decomp H. assert (p : S x0<S n). lia. ex (S x0) p x2. simpl. assert (NatCompat.lt_S_n p = x1). apply lt_unique. rewrite H. subst x. auto. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)