\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 ]} . <{({(x) . (x)} . ts ) . ({({((p) . y ) . ((p) . y )} . ts ) . ({((p) . y ) . ((p) . y )} . ts )} . pl )} . is > . {({(q) . (x) . (p)} . t11 ) . (({((p) . y ) . ((p) . y )} . ts ) . t1 ) . ({(x) . (x)} . ts ) . ({({((p) . y ) . ((p) . y )} . ts ) . (( 1 ) . suc )} . ts ) . ({({((p) . y ) . ((p) . y )} . ts ) . ({((p) . y ) . ((p) . y )} . ts )} . pl ) . ( nat )} . tris

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