proposition: Lemma In_reducts_vec_intro : forall f ts t i (p : i < arity f), In t (reducts (Vnth ts p)) -> In (Fun f (Vreplace ts p t)) (reducts_vec f ts ts (Nat.le_refl (arity f))).
proof: Proof. intros. assert (q : arity f - arity f + i < arity f). lia. assert (Vreplace ts p t = Vreplace ts q t). apply Vreplace_pi. lia. rewrite H0. apply In_reducts_vec_intro_aux with (p := p). hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)