λδ digital library (LDDL)
Constant
Informal description: ""
{λ[sigma:Set].λ[p:∀[x:sigma].Prop].λ[a1:{(p).(sigma)}.amone].λ[s:{(p).(sigma)}.some]}.<{(p).(sigma)}.one>.{(s).(a1).({(p).(sigma)}.some).({(p).(sigma)}.amone)}.andi Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100