Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as')) (recursive)

Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B