n:{1...}, A:Type, R:(A
AProp).
(
n ~ A) 
(EquivRel x,y:A. x R y)
(x,y:A. Dec(x R y)) (
m:(n+1). m ~ (x,y:A//(x R y)))
quotient_of_finite
P
Thm* n:{1...}, A:Type, R:(AAProp).
(n ~ A)
(EquivRel x,y:A. x R y)
(x,y:A. Dec(x R y)) (m:(n+1). m ~ (x,y:A//(x R y)))
quotient_of_finite
Thm* n:{1...}, E:(nnProp).
(EquivRel x,y:n. x E y) & (x,y:n. Dec(x E y))
(m:(n+1). m ~ (i,j:n//(i E j)))
quotient_of_nsubn