Lemma subtype_complement_intersection_empty {S} {I : UU} {f : I -> hsubtype X} : (∑ i : I, f i = S) -> (∑ j : I, f j = subtype_complement S) -> subtype_intersection f ≡ emptysubtype _. Proof. intros has_S has_neg_S x; use make_dirprod. - intros in_intersection. pose (in_S := in_intersection (pr1 has_S)). pose (in_neg_S := in_intersection (pr1 has_neg_S)). cbn in *. pose (in_S' := (eqtohomot (pr2 has_S)) x). pose (in_neg_S' := (eqtohomot (pr2 has_neg_S)) x). apply (not_in_subtype_and_complement S x). + abstract (induction in_S'; assumption). + abstract (induction in_neg_S'; assumption). - intros empt; induction empt. Qed.