proposition: Lemma IPHP_with_2_holes (P : Pinf W) (f : elts P -> bool) : exists b (Q : Pinf P), forall x (i : mem x Q), f (elt (Pinf_sub Q _ i)) = b.
proof: Proof. destruct P as [P [PW Pinf]]; simpl in *. assert (e : P [=] union (fiber f true) (fiber f false)). intro x. repeat unfold mem, union, fiber. split. intro xP. case_eq (f (elt xP)); intro f_x. left. ex xP. hyp. right. ex xP. hyp. intros [[xP _]|[xP _]]; hyp. rewrite e, infinite_union in Pinf. destruct Pinf as [f_true_inf|f_false_inf]. assert (h : fiber f true [<=] P). fo. ex true (mk_Pinf h f_true_inf). intros x [xP hx]. rewrite (proof_irrelevance _ _ xP). hyp. assert (h : fiber f false [<=] P). fo. ex false (mk_Pinf h f_false_inf). intros x [xP hx]. rewrite (proof_irrelevance _ _ xP). hyp. Qed.
imports: Coq(Morphisms Basics Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil DepChoice LogicUtil SetUtil FinSet InfSet NatUtil)