proposition: Lemma union_quot_lE' (x: S+T): union_quot_l^-1 (\pi x) = match x with inl y => inl (\pi y) | inr y => inr y end.
proof: Proof. case x=>y. by rewrite -(union_quot_lEl y) bijK. by rewrite -(union_quot_lEr y) bijK. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)