proposition: Lemma reducts_complete : rules_preserve_vars R -> forall t u, red R t u -> In u (reducts t).
proof: Proof. intros H t; pattern t; apply term_ind_forall; clear t; intros. ded (red_case H0). split_all. simpl. apply top_reducts_complete; hyp. decomp H2. discr. rewrite reducts_fun, in_app. ded (red_case H1). split_all. left. apply top_reducts_complete; hyp. right. Funeqtac. subst x0. ded (Vforall_nth x2 H0). subst u. apply In_reducts_vec_intro. apply H2. hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)