\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 ] . λ[y: nat ] . λ[z: nat ] . λ[p:{(z) . (y) . (x)} . prop1 ]} . <{((z) . suc ) . (y) . (x)} . prop1 > . {({({(z) . (y)} . satz28f ) . (x) . ({((z) . suc ) . (y)} . ts ) . ({(y) . ({(z) . (y)} . ts )} . pl )} . ists2 ) . ({(y) . ({(z) . (y)} . ts ) . (x)} . distpt2 ) . ({(p) . ({(y) . (x)} . ts ) . ({({(z) . (y)} . ts ) . (x)} . ts ) . ({(z) . ({(y) . (x)} . ts )} . ts )} . ispl1 ) . ({(z) . ({(y) . (x)} . ts )} . satz28b ) . ({({((z) . suc ) . (y)} . ts ) . (x)} . ts ) . ({({(y) . ({(z) . (y)} . ts )} . pl ) . (x)} . ts ) . ({({(y) . (x)} . ts ) . ({({(z) . (y)} . ts ) . (x)} . ts )} . pl ) . ({({(y) . (x)} . ts ) . ({(z) . ({(y) . (x)} . ts )} . ts )} . pl ) . ({((z) . suc ) . ({(y) . (x)} . ts )} . ts ) . ( nat )} . tr4is

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