λδ digital library (LDDL)
Constant
Informal description: ""
{λ[p:∀[x:natt].Prop].λ[s:(p).some]}.<(λ[x:natt].{(x).(p)}.min).some>.{(λ[x:nat].λ[y:{(x).({(s).(p)}.q)}.min].{(y).(x).(s).(p)}.t14).((λ[x:natt].{(x).(p)}.min).some).({(s).(p)}.t4).(λ[x:nat].{(x).({(s).(p)}.q)}.min).(nat)}.someapp Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100