proposition: Lemma union_quot_lEl (x: S): union_quot_l (inl (\pi x)) = \pi (inl x).
proof: Proof. simpl. apply /eqquotP. apply piK. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)