λδ digital library (LDDL)
Constant
Informal description: ""
{λ[x:frac].λ[y:frac].λ[v:frac].λ[w:frac].λ[e:{(x).({(v).(y)}.pf)}.eq].λ[f:{(x).({(w).(y)}.pf)}.eq]}.<{(w).(v)}.eq>.{({(f).(e).(x).({(w).(y)}.pf).({(v).(y)}.pf)}.treq2).(y).(w).(v)}.satz63e Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100