\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 ] . λ[u: nat ] . λ[i:{({(u) . ((p) . y )} . pl ) . (x)} . is ] . λ[t: nat ] . λ[j:{({(t) . (u)} . pl ) . ((p) . y )} . is ]} . <{({({({(t) . (t)} . ts ) . ({(u) . (u)} . ts )} . pl ) . ({({({(u) . ((p) . y )} . ts ) . (( 1 ) . suc )} . ts ) . ({((p) . y ) . ((p) . y )} . ts )} . pl )} . pl ) . ({({(t) . (t)} . ts ) . ({(x) . (x)} . ts )} . pl )} . is > . {({({(t) . (t)} . ts ) . ({(u) . (u)} . ts ) . ({({({(u) . ((p) . y )} . ts ) . (( 1 ) . suc )} . ts ) . ({((p) . y ) . ((p) . y )} . ts )} . pl )} . asspl1 ) . ({({(j) . (t) . (i) . (u) . (q) . (x) . (p)} . t19 ) . ({(t) . (t)} . ts ) . ({({(u) . (u)} . ts ) . ({({({(u) . ((p) . y )} . ts ) . (( 1 ) . suc )} . ts ) . ({((p) . y ) . ((p) . y )} . ts )} . pl )} . pl ) . ({(x) . (x)} . ts )} . ispl1 ) . ({({({(t) . (t)} . ts ) . ({(u) . (u)} . ts )} . pl ) . ({({({(u) . ((p) . y )} . ts ) . (( 1 ) . suc )} . ts ) . ({((p) . y ) . ((p) . y )} . ts )} . pl )} . pl ) . ({({(t) . (t)} . ts ) . ({({(u) . (u)} . ts ) . ({({({(u) . ((p) . y )} . ts ) . (( 1 ) . suc )} . ts ) . ({((p) . y ) . ((p) . y )} . ts )} . pl )} . pl )} . pl ) . ({({(t) . (t)} . ts ) . ({(x) . (x)} . ts )} . pl ) . ( nat )} . tris

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