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