\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 ] . λ[s:sigma] . λ[t:sigma]} . <{({({(t) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . ectelt ) . ({(s) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . ectelt ) . (ff2) . (fu2) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . indeq2 ) . ((t) . (s) . fu2) . (alpha)} . is > . {({(t) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . th5 ) . (t) . ({(s) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . th5 ) . (s) . ({(t) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . ectelt ) . ({(s) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . ectelt ) . (ff2) . (fu2) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . th1

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