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
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* f:(AB), R:(BBProp).
Bij(A; B; f)
(EquivRel x,y:B. x R y)
(F:((x,y:A//(x R_f y))(x,y:B//(x R y))).
Bij(x,y:A//(x R_f y); x,y:B//(x R y); F))
quotient_1_1_corr
Thm* f:(AB), R:(BBProp).
(EquivRel x,y:B. x R y) (EquivRel x,y:A. x R_f y)
preima_of_equiv_rel
Thm* R:(TTProp).
(EquivRel x,y:T. x R y)
(Q:((x,y:T//(x R y))(x,y:T//(x R y))Prop).
(EquivRel u,v:x,y:T//(x R y). u Q v)
((x,y:T//(x Q y)) ~ (u,v:(x,y:T//(x R y))//(u Q v))))
quo_of_quo
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* R:(TTProp).
(EquivRel x,y:T. x R y)
(Q:((x,y:T//(x R y))(x,y:T//(x R y))Prop).
(EquivRel u,v:x,y:T//(x R y). u Q v) (EquivRel x,y:T. x Q y))
incl_aux6_quo
Thm* E:(TTProp).
(EquivRel x,y:T. x E y) (x,y:T. x = y x = y 
u,v:T//(u E v))
incl_aux5_quo
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