\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 ] . λ[n:({({(l) . (y) . (p) . (x)} . yy1 ) . (({(l) . (y) . (p) . (x)} . xxs ) . f) . ((y) . 1to )} . is ) . not ]} . <{({(l) . (y) . (p) . (x)} . yy1 ) . (({(l) . (y) . (p) . (x)} . xxs ) . {(n) . (b) . (f) . (l) . (y) . (p) . (x)} . f2 ) . ((y) . 1to )} . is > . {({(n) . (b) . (f) . (l) . (y) . (p) . (x)} . t60 ) . ({(n) . (b) . (f) . (l) . (y) . (p) . (x)} . t61 ) . (({(n) . (b) . (f) . (l) . (y) . (p) . (x)} . m0 ) . f) . ({(l) . (y) . (p) . (x)} . yy1 ) . (({(l) . (y) . (p) . (x)} . xxs ) . {(n) . (b) . (f) . (l) . (y) . (p) . (x)} . f2 ) . ((y) . 1to )} . tris2

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