\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 ]} . <{({({(u) . (u)} . ts ) . ({(t) . (t)} . ts )} . fr ) . ({( 1 ) . (( 1 ) . suc )} . fr )} . eq > . {({( 1 ) . (( 1 ) . suc ) . ({(u) . (u)} . ts ) . ({(t) . (t)} . ts )} . 12isnd ) . (({(t) . (t)} . ts ) . satz28e ) . ({({(j) . (t) . (i) . (u) . (q) . (x) . (p)} . t29 ) . ({({(u) . (u)} . ts ) . (( 1 ) . suc )} . ts ) . ({(t) . (t)} . ts ) . ( nat )} . symis ) . ({({(u) . (u)} . ts ) . ({(t) . (t)} . ts ) . ( 1 ) . (( 1 ) . suc )} . ndis12 ) . ({(({( 1 ) . (( 1 ) . suc )} . fr ) . den ) . (({({(u) . (u)} . ts ) . ({(t) . (t)} . ts )} . fr ) . num )} . ts ) . ({( 1 ) . ({(t) . (t)} . ts )} . ts ) . ({(t) . (t)} . ts ) . ({({(u) . (u)} . ts ) . (( 1 ) . suc )} . ts ) . ({(({({(u) . (u)} . ts ) . ({(t) . (t)} . ts )} . fr ) . den ) . (({( 1 ) . (( 1 ) . suc )} . fr ) . num )} . ts ) . ( nat )} . tr4is

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