L A*Prop

A*A*Prop

n ~ (x,y:A*//(x R y))

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

(x,y:A*//(x R y))

l:A*. L(l) g(l)

x,y:x,y:A*//(x R y). Dec(x Rg y)

m:. m ~ (x,y:A*//(x L-induced Equiv y))

Inst Thm* L:LangOver(A). EquivRel x,y:A*. x L-induced Equiv y [A;L]

1	12. EquivRel x,y:A*. x L-induced Equiv y m:. m ~ (x,y:A*//(x L-induced Equiv y))

About: