fact: Fixpoint reducts2 t := match t with | Var _ => top_reducts R t | Fun f ts => let fix reducts2_vec k (us : terms k) : list (terms k) := match us with | Vnil => nil | Vcons u1 us' => map (fun x => Vcons x us') (reducts2 u1) ++ map (fun x => Vcons u1 x) (reducts2_vec _ us') end in top_reducts R t ++ map (Fun f) (reducts2_vec (arity f) ts) end.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)