n:{1...}, A:Type, L:LangOver(A), R:(A*
A*Prop).
Fin(A) 
(EquivRel x,y:A*. x R y)
(
n ~ (x,y:A*//(x R y)))
(x,y,z:A*. (x R y) ((z @ x) R (z @ y)))
(
g:((x,y:A*//(x R y))
). l:A*. L(l) 
g(l))
(m:. m ~ (x,y:A*//(x L-induced Equiv y))) & (l:A*. Dec(L(l)))
mn_23