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
| i
j }
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
Thm* n:{1...}, m:n, E:(nnProp).
(EquivRel x,y:n. x E y) (EquivRel x,y:m. x E y)
rest_equi_rel
Thm* n:{1...}, m:n, E:(nnProp).
Trans x,y:n. x E y Trans x,y:m. x E y
rest_tran_rel
Thm* n:{1...}, m:n, E:(nnProp). Sym x,y:n. x E y Sym x,y:m. x E y
rest_symm_rel
Thm* n:{1...}, m:n, E:(nnProp). Refl(n;x,y.x E y) Refl(m;x,y.x E y)
rest_refl_rel
Thm* n:{1...}, E:(nnProp).
(EquivRel i,j:n. i E j)
(x:i,j:n//(i E j). 
x = n-1 
i,j:n//(i E j) x i,j:(n-1)//(i E j))
incl_aux4_quo
Thm* n:{1...}, m:n, E:(nnProp).
(EquivRel i,j:n. i E j)
(x,y:i,j:m//(i E j). x = y i,j:n//(i E j) 
x = y)
incl_aux3_quo
Thm* n:{1...}, m:n, E:(nnProp).
(EquivRel x,y:n. x E y) (z:x,y:m//(x E y). z x,y:n//(x E y))
incl_aux2_quo