proposition: Lemma setU_setQ: union (quotient r) = substrate r.
proof: Proof. set_extens t => ts. move: (setU_hi ts) => [z tz zu]; apply: (inc_in_setQ_sr tz zu). apply: (@setU_i _ (class r t)); [ apply/class_P; equiv_tac | fprops]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)