proposition: Lemma In_reducts_vec_elim : forall v' f ts, In v' (reducts_vec f ts ts (Nat.le_refl (arity f))) -> exists i, exists p : i < arity f, exists u', In u' (reducts (Vnth ts p)) /\ v' = Fun f (Vreplace ts p u').
proof: Proof. intros. apply In_reducts_vec_elim_aux with (k := arity f) (us := ts) (h := Nat.le_refl (arity f)). intros. assert (r : arity f - arity f + i < arity f). lia. exists r. apply Vnth_eq. lia. hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)