An exact proof term for the current goal is (SepI (finite_intersections_of X S) (λb : set ⇒ b ≠ Empty) (intersection_of_family X F) (ReplI (finite_subcollections S) (λF0 : set ⇒ intersection_of_family X F0) F HF) Hnon).