λδ digital library (LDDL)
Constant
Informal description: ""
λ[i:{(1t).(2t).((2).1to)}.is].<{((1t).u0).((2t).u0)}.is>.{(i).(1t).(2t).(λ[x:nat].{(2).(x)}.lessis).(nat)}.isini Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100