fact: Fixpoint reducts t := match t with | Var _ => top_reducts R t | Fun f ts => let fix reducts_vec k (us : terms k) : k <= arity f -> list term := match us in vector _ k return k <= arity f -> list term with | Vnil => fun _ => nil | Vcons u1 us' => fun h => map (fun x => Fun f (Vreplace ts (reducts_aux2 h) x)) (reducts u1) ++ reducts_vec _ us' (reducts_aux1 h) end in top_reducts R t ++ reducts_vec (arity f) ts (Nat.le_refl (arity f)) end.
imports: CoLoR(LogicUtil ATrs RelUtil ListUtil VecUtil AMatching NatUtil)