\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] . λ[fu:Π[x:sigma] . alpha] . λ[ff:{(fu) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . fixfu ] . λ[e:{(trr1) . (symr1) . (refr1) . (r) . (sigma)} . ect ] . λ[a1:alpha] . λ[b1:alpha] . λ[pa1:{(a1) . (e) . (ff) . (fu) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . prop2 ] . λ[pb1:{(b1) . (e) . (ff) . (fu) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . prop2 ] . λ[s:sigma] . λ[pa1s:{(s) . (a1) . (e) . (ff) . (fu) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . prop1 ] . λ[t:sigma] . λ[pb1t:{(t) . (b1) . (e) . (ff) . (fu) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . prop1 ]} . <(t) . (s) . r> . {({(pb1t) . (t) . (pa1s) . (s) . (pb1) . (pa1) . (b1) . (a1) . (e) . (ff) . (fu) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . t6 ) . (t) . ({(pb1t) . (t) . (pa1s) . (s) . (pb1) . (pa1) . (b1) . (a1) . (e) . (ff) . (fu) . (alpha) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . t5 ) . (s) . (e) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . th7

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