\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] . λ[r:∀[x:sigma] . ∀[y:sigma] . Prop] . λ[refr1:∀[x:sigma] . (x) . (x) . r] . λ[symr1:∀[x:sigma] . ∀[y:sigma] . ∀[t:(y) . (x) . r] . (x) . (y) . r] . λ[trr1:∀[x:sigma] . ∀[y:sigma] . ∀[z:sigma] . ∀[t:(y) . (x) . r] . ∀[u:(z) . (y) . r] . (z) . (x) . r] . λ[alpha:Set] . λ[fu2:Π[x:sigma] . Π[y:sigma] . alpha] . λ[ff2:{(fu2) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . fixfu2 ] . λ[e:{(trr1) . (symr1) . (refr1) . (r) . (sigma)} . ect ] . λ[s:sigma] . λ[t:sigma] . λ[tsr:(t) . (s) . r] . λ[u:sigma] . λ[uee:{({(e) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . ecect ) . (u) . (sigma)} . esti ]} . <{((t) . {(e) . (ff2) . (fu2) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . i ) . ((t) . (u) . fu2) . (alpha)} . is > . {(t) . ({(uee) . (u) . (tsr) . (t) . (s) . (e) . (ff2) . (fu2) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . t3 ) . ({(e) . (ff2) . (fu2) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . i ) . ((u) . fu2) . (alpha) . (sigma)} . fise

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