proposition: Lemma In_reducts_vec_intro_aux : forall f ts k (us : terms k) (h : k <= arity f) t i (p : i < k) (q : arity f - k + i < arity f), In t (reducts (Vnth us p)) -> In (Fun f (Vreplace ts q t)) (reducts_vec f ts us h).
proof: Proof. induction us. intros. lia. intros g t. simpl. set (F := fun x : term => Fun f (Vreplace ts (reducts_aux2 g) x)). destruct i; intros p q; rewrite in_app. left. assert (e : arity f - S n + 0 = arity f - S n). lia. rewrite (Vreplace_pi ts q (reducts_aux2 g) t e). apply in_map with (f:=F). hyp. right. assert (q' : arity f - n + i < arity f). lia. assert (Vreplace ts q t = Vreplace ts q' t). apply Vreplace_pi. lia. rewrite H0. apply IHus with (p := NatCompat.lt_S_n p). hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)