proposition: Lemma noid_inl_sumP x: inc x noid_inl_sum <-> [/\ pairp x, inc (Q x) I & inc (P x) (Vg E (Q x))].
proof: Proof. split; first by case/disjointU_P; rewrite domain_E. by move => [ha hb hc]; apply /disjointU_P; rewrite domain_E. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)