proposition: Lemma reducts_correct : forall t u, In u (reducts t) -> red R t u.
proof: Proof. intro t. pattern t; apply term_ind_forall; clear t. intros. apply top_reducts_correct_red. hyp. intros f ts IH u. rewrite reducts_fun, in_app. split_all. apply hd_red_incl_red. apply top_reducts_correct. hyp. rename H into h. ded (In_reducts_vec_elim h). decomp H. ded (Vforall_nth x0 IH _ H1). redtac. unfold red. ex l r. assert (h1 : 0+x<=arity f). lia. set (v1 := Vsub ts h1). assert (h2 : S x+(arity f-S x)<=arity f). lia. set (v2 := Vsub ts h2). assert (e : x+S(arity f-S x)=arity f). lia. exists (Cont f e v1 c v2). exists s. split_all. simpl. apply args_eq. rewrite <- xl. unfold v2. rewrite Vcons_nth. unfold v1. apply Veq_app_cons_aux. simpl. rewrite H2. apply args_eq. apply Veq_nth; intros. rewrite Vnth_cast, Vnth_app. destruct (le_gt_dec x i). destruct (eq_nat_dec x i). set (q := Vnth_app_aux (S (arity f - S x)) (Vnth_cast_aux e ip) l0). gen q. assert (i - x = 0). subst; clear; lia. rewrite H. intro. simpl. trans (Vnth (Vreplace ts x0 x1) x0). apply Vnth_eq. auto. rewrite Vnth_replace. hyp. rewrite Vnth_replace_neq. 2: hyp. rewrite (Veq_app_cons ts x0), Vnth_cast, Vnth_app. destruct (le_gt_dec x i). 2: lia. rewrite !Vnth_cons. destruct (lt_ge_dec 0 (i-x)). unfold v2. rewrite !Vnth_sub. apply Vnth_eq. refl. lia. rewrite Vnth_replace_neq. 2: lia. rewrite (Veq_app_cons ts x0), Vnth_cast, Vnth_app. destruct (le_gt_dec x i). lia. assert (g0 = g). apply lt_unique. subst g0. assert (Vsub ts (Veq_app_cons_aux1 x0) = v1). unfold v1. f_equal. apply le_unique. rewrite H. refl. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)