proposition: Lemma quot_union_KE (x: S+K): quot_union_K (\pi x) = \pi (sum_left k x).
proof: Proof. simpl. generalize (piK e x). case (repr (pi e x)); case x => z y H/=. by apply /eqquotP. move: H=>/eqquotP H. rewrite kh in H. apply /eqquotP. rewrite /=map_equivE. by apply /eqquotP. all: apply /eqquotP; rewrite /=map_equivE; apply /eqquotP; rewrite -!kh; by apply /eqquotP. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)