fact: Fixpoint 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.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)