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