fact: Definition merge_union_bwd (x : sig (U :|: V)) : sig U + sig V := match setU_dec (valP x) with | inl p => inl (Sub (val x) p) | inr p => inr (Sub (val x) p.2) end.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)