\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 ] . λ[v:({(l) . (y) . (p) . (x)} . ym1 ) . 1to ]} . <{(y) . ({(v) . (i) . (b) . (f) . (l) . (y) . (p) . (x)} . v1 )} . less > . {({(l) . (y) . (p) . (x)} . t18 ) . ({(v) . ({(l) . (y) . (p) . (x)} . ym1 )} . 1top ) . (y) . ({(l) . (y) . (p) . (x)} . ym1 ) . ({(v) . (i) . (b) . (f) . (l) . (y) . (p) . (x)} . v1 )} . satz16a

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