proposition: Lemma sumUx {A}: bij (void + A) A.
proof: Proof. exists (fun x => match x with inl x => vfun x | inr a => a end) (fun x => inr x); abstract by repeat case. Defined.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)