proposition: Lemma In_reducts_vec_elim_aux : forall v' f ts k (us : terms k), (forall i (p : i < k), exists r : arity f - k + i < arity f, Vnth us p = Vnth ts r) -> forall h, In v' (reducts_vec f ts us h) -> exists i, exists p : i < arity f, exists u', In u' (reducts (Vnth ts p)) /\ v' = Fun f (Vreplace ts p u').
proof: Proof. induction us. contr. intros E g H. simpl in H. rewrite in_app in H. split_all. ded (in_map_elim H). decomp H0. destruct (E 0 (Nat.lt_0_succ n)). simpl in H0. ex (arity f - S n + 0) x0 x. rewrite <- H0. split_all. rewrite H3. apply args_eq. apply Vreplace_pi. lia. assert (E' : forall (i : nat) (p : i < n), exists r : arity f - n + i < arity f, Vnth us p = Vnth ts r). intros. assert (p' : S i < S n). lia. destruct (E (S i) p'). simpl in H. assert (NatCompat.lt_S_n p' = p). apply lt_unique. simpl in H0. rewrite H1 in H0. rewrite H0. assert (r : arity f - n + i < arity f). lia. exists r. apply Vnth_eq. lia. assert (h' : n <= arity f). lia. rewrite reducts_vec_pi with (h':=h') in H. apply IHus with (h:=h'); hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)