λδ digital library (LDDL)
Constant
Informal description: ""
{λ[a:Prop].λ[ksi:Set].λ[x:ksi].λ[y:ksi].λ[n:(a).not].λ[x1:ksi].λ[y1:ksi].λ[px1:{(x1).(y).(x).(ksi).(a)}.prop1].λ[py1:{(y1).(y).(x).(ksi).(a)}.prop1]}.<{(y1).(x1).(ksi)}.is>.{({(py1).(px1).(y1).(x1).(n).(y).(x).(ksi).(a)}.t13).({(py1).(px1).(y1).(x1).(n).(y).(x).(ksi).(a)}.t12).(y).(y1).(x1).(ksi)}.tris2 Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100