Lemma subtype_complement_union {S} (lem : LEM) {I : UU} {f : I -> hsubtype X} : (∑ i : I, f i = S) -> (∑ j : I, f j = subtype_complement S) -> subtype_union f ≡ totalsubtype _. Proof. intros has_S has_neg_S x; use make_dirprod. - intro; exact tt. - intro. induction (lem (S x)). + apply hinhpr. exists (pr1 has_S). abstract (rewrite (pr2 has_S); assumption). + apply hinhpr. exists (pr1 has_neg_S). abstract (rewrite (pr2 has_neg_S); assumption). Qed.