\lambda\delta home page

home	news	documentation	specification		implementation
foreword	milestones	version 2	version 2	(background - core - applications)	library	(static LDDL directory)
citations	visibility	version 1	version 1	(static HELM directory)	helena

Informal description: ""

{λ[x: nat ] . λ[p:(x) . prop2 ] . λ[y: nat ] . λ[l:{(y) . ((x) . suc )} . less ] . λ[f:Π[t:((x) . xs ) . 1to ] . (y) . 1to ] . λ[b:{(f) . ((y) . 1to ) . (((x) . xs ) . 1to )} . bijective ] . λ[i:{({(l) . (y) . (p) . (x)} . yy1 ) . (({(l) . (y) . (p) . (x)} . xxs ) . f) . ((y) . 1to )} . is ] . λ[u:(x) . 1to ]} . <{({( 1 ) . ({(l) . (y) . (p) . (x)} . ym1 )} . pl ) . ({( 1 ) . ({(u) . (i) . (b) . (f) . (l) . (y) . (p) . (x)} . w1 )} . pl )} . lessis > . {({({(u) . (i) . (b) . (f) . (l) . (y) . (p) . (x)} . t30 ) . ({(u) . (i) . (b) . (f) . (l) . (y) . (p) . (x)} . w1 ) . (y)} . satz25b ) . ({({(l) . (y) . (p) . (x)} . t15 ) . ( 1 ) . (y)} . th1c ) . ({( 1 ) . ({(u) . (i) . (b) . (f) . (l) . (y) . (p) . (x)} . w1 )} . pl ) . ({( 1 ) . ({(l) . (y) . (p) . (x)} . ym1 )} . pl ) . (y)} . islessis2

Validation parameters: sort hierarchy = "Z2", kernel options = ""