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

{λ[p: prop3 ] . λ[x: nat ] . λ[q:{(x) . ((p) . y )} . prop1 ]} . <{({({((p) . y ) . (( 1 ) . suc )} . ts ) . ({((p) . y ) . (( 1 ) . suc )} . ts )} . ts ) . ({(x) . (x)} . ts )} . less > . {({(((p) . y ) . t2 ) . ({({({((p) . y ) . (( 1 ) . suc )} . ts ) . ( nat )} . refis ) . ({((p) . y ) . (( 1 ) . suc )} . ts ) . ({((p) . y ) . (( 1 ) . suc )} . ts )} . lessisi2 ) . ({((p) . y ) . (( 1 ) . suc )} . ts ) . ((p) . y ) . ({((p) . y ) . (( 1 ) . suc )} . ts ) . ({((p) . y ) . (( 1 ) . suc )} . ts )} . satz35c ) . ({({(q) . (x) . (p)} . t11 ) . ({((p) . y ) . ((p) . y ) . (( 1 ) . suc )} . assts1 ) . ({(x) . (x)} . ts ) . ({({((p) . y ) . ((p) . y )} . ts ) . (( 1 ) . suc )} . ts ) . ({((p) . y ) . ({((p) . y ) . (( 1 ) . suc )} . ts )} . ts ) . ( nat )} . tris ) . ({({((p) . y ) . (( 1 ) . suc )} . ts ) . ({((p) . y ) . (( 1 ) . suc )} . ts )} . ts ) . ({(x) . (x)} . ts ) . ({((p) . y ) . ({((p) . y ) . (( 1 ) . suc )} . ts )} . ts )} . isless1

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