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