\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: ""

{λ[alpha:Set] . λ[x: nat ] . λ[y: nat ] . λ[i:{(x) . (y)} . is ] . λ[f:Π[t:(y) . 1to ] . alpha] . λ[u:(y) . 1to ]} . <{({({(u) . ({(f) . (i) . (y) . (x) . (alpha)} . t4 ) . (y) . (x)} . left1to ) . ({(f) . (i) . (y) . (x) . (alpha)} . t5 ) . (x) . (y)} . left1to ) . (u) . ((y) . 1to )} . is > . {({({(u) . (f) . (i) . (y) . (x) . (alpha)} . t6 ) . ({({(f) . (i) . (y) . (x) . (alpha)} . t5 ) . ({({(u) . ({(f) . (i) . (y) . (x) . (alpha)} . t4 ) . (y) . (x)} . left1to ) . (x)} . 1top ) . (y) . (x) . ({({(u) . ({(f) . (i) . (y) . (x) . (alpha)} . t4 ) . (y) . (x)} . left1to ) . (x)} . inn )} . trlessis ) . ({({(u) . ({(f) . (i) . (y) . (x) . (alpha)} . t4 ) . (y) . (x)} . left1to ) . (x)} . inn ) . ({(u) . (y)} . 1top ) . ({(u) . (y)} . inn ) . (y)} . isoutni ) . ({(u) . (y)} . isoutinn ) . ({({(u) . ({(f) . (i) . (y) . (x) . (alpha)} . t4 ) . (y) . (x)} . left1to ) . ({(f) . (i) . (y) . (x) . (alpha)} . t5 ) . (x) . (y)} . left1to ) . ({({(u) . (y)} . 1top ) . ({(u) . (y)} . inn ) . (y)} . outn ) . (u) . ((y) . 1to )} . tris

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