fact: Fixpoint subterm_lst t := match t with | Var _ => nil | Fun f ts => let fix subterm_lst_vec k (us : terms k) {struct us} : list term := match us with | Vnil => nil | Vcons u1 us' => subterm_lst u1 ++ subterm_lst_vec _ us' end in list_of_vec ts ++ subterm_lst_vec (arity f) ts end.
imports: CoLoR(AContext VecUtil ListUtil LogicUtil NatUtil RelUtil ASN)