Alph*Alph*Prop

Alph*

x:Alph*. R(x,x)

x,y:Alph*. R(x,y) R(y,x)

x,y,z:Alph*. R(x,y) & R(y,z) R(x,z)

x,y,z:Alph*. R(x,y) R((z @ x),z @ y)

w:(nAlph*). l:Alph*. i:n. R(l,w(i))

v:(mAlph*). l:Alph*. L(l) (i:m. R(l,v(i)))

x,y:Alph*. Dec(l:Alph*. L(l @ x) = L(l @ y))

Dec(x@0:Alph*. L(x@0 @ x) = L(x@0 @ y))

None

About: