\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 ]} . <{({(x) . (x)} . ts ) . ({({((p) . y ) . ((p) . y )} . ts ) . (( 1 ) . suc )} . ts )} . is > . {(({(x) . (x)} . ts ) . satz28a ) . ({( 1 ) . (( 1 ) . suc ) . ({((p) . y ) . ((p) . y )} . ts ) . ({(x) . (x)} . ts )} . ndis12 ) . ({(q) . (x) . (p)} . t10 ) . ({({((p) . y ) . ((p) . y )} . ts ) . ({(x) . (x)} . ts ) . ( 1 ) . (( 1 ) . suc )} . 12isnd ) . ({(x) . (x)} . ts ) . ({( 1 ) . ({(x) . (x)} . ts )} . ts ) . ({(({( 1 ) . (( 1 ) . suc )} . fr ) . den ) . (({({((p) . y ) . ((p) . y )} . ts ) . ({(x) . (x)} . ts )} . fr ) . num )} . ts ) . ({(({({((p) . y ) . ((p) . y )} . ts ) . ({(x) . (x)} . ts )} . fr ) . den ) . (({( 1 ) . (( 1 ) . suc )} . fr ) . num )} . ts ) . ({({((p) . y ) . ((p) . y )} . ts ) . (( 1 ) . suc )} . ts ) . ( nat )} . tr4is

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