fact: Definition union_equiv_l_rel: rel (S+T) := fun x y => match x,y with | inl x,inl y => e x y | inr x,inr y => x==y | _,_ => false end.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)