No other cites to report in MarkB_generic
for_hdtl	Def ForHdTl{A,f,k} h::t as. g(h;t) == reduce(f;k;mapcons(h,t. g(h;t);as))
	Thm* A,B,C:Type, f:(BCC), k:C, as:A List, g:(A(A List)B). (ForHdTl{A,f,k} h::t as. g(h,t)) C
mapcons	Def mapcons(f;as) == Case of as; nil nil ; a.as' [(f(a,as')) / mapcons(f;as')] (recursive)
	Thm* A,B:Type, f:(A(A List)B), l:A List. mapcons(f;l) B List
reduce	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

Syntax:

ForHdTl{A,f,k} h::t as. g(h;t)

has structure:

for_hdtl(A; f; k; as; h,t.g(h;t))

About: