n:{1...}, m:
n, E:(n
nProp).
(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
Q == (P Q) & (P Q)
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
In prior sections: core well fnd int 1 bool 1 rel 1 quot 1 int 2 fun 1