\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 ]} . <{({(l) . (y) . (p) . (x)} . ym1 ) . (x)} . prop1 > . {({(i) . (b) . (f) . (l) . (y) . (p) . (x)} . t57 ) . ({(i) . (b) . (f) . (l) . (y) . (p) . (x)} . f1 ) . (λ[g:Π[t:(x) . 1to ] . ({(l) . (y) . (p) . (x)} . ym1 ) . 1to ] . {(g) . (({(l) . (y) . (p) . (x)} . ym1 ) . 1to ) . ((x) . 1to )} . bijective ) . (Π[t:(x) . 1to ] . ({(l) . (y) . (p) . (x)} . ym1 ) . 1to )} . somei

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