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

{λ[sigma:Set] . λ[p:∀[x:sigma] . Prop] . λ[o1:{(p) . (sigma)} . ot ]} . <{({({(o1) . (p) . (sigma)} . inp ) . ({(o1) . (p) . (sigma)} . in ) . (p) . (sigma)} . out ) . (o1) . ({(p) . (sigma)} . ot )} . is > . {({({({(o1) . (p) . (sigma)} . in ) . (sigma)} . refis ) . ({({(o1) . (p) . (sigma)} . inp ) . ({(o1) . (p) . (sigma)} . in ) . (p) . (sigma)} . otax2 ) . ({(o1) . (p) . (sigma)} . in ) . ({(o1) . (λ[x:{(p) . (sigma)} . ot ] . {(x) . (p) . (sigma)} . in ) . (sigma) . ({(p) . (sigma)} . ot )} . imagei ) . ({(o1) . (p) . (sigma)} . in ) . ({(p) . (sigma)} . otax1 ) . (λ[x:{(p) . (sigma)} . ot ] . {(x) . (p) . (sigma)} . in ) . (sigma) . ({(p) . (sigma)} . ot )} . isinv ) . ({(o1) . ({(p) . (sigma)} . otax1 ) . (λ[x:{(p) . (sigma)} . ot ] . {(x) . (p) . (sigma)} . in ) . (sigma) . ({(p) . (sigma)} . ot )} . isst1 ) . ({({(o1) . (p) . (sigma)} . inp ) . ({(o1) . (p) . (sigma)} . in ) . (p) . (sigma)} . out ) . ({({(o1) . (λ[x:{(p) . (sigma)} . ot ] . {(x) . (p) . (sigma)} . in ) . (sigma) . ({(p) . (sigma)} . ot )} . imagei ) . ({(o1) . (p) . (sigma)} . in ) . ({(p) . (sigma)} . otax1 ) . (λ[x:{(p) . (sigma)} . ot ] . {(x) . (p) . (sigma)} . in ) . (sigma) . ({(p) . (sigma)} . ot )} . soft ) . (o1) . ({(p) . (sigma)} . ot )} . tris

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