proposition: Lemma set_coinfinite_fresh (s: nat -> Prop) (COINF: set_coinfinite s) : exists b, ~ s b /\ set_coinfinite (s ∪₁ eq b).
proof: Proof. repeat autounfold with unfolderDb in *. tertium_non_datur (forall b, s b). by destruct COINF; exists nil; ins; desf. exists n; splits; red; ins; desf. apply COINF; exists (n :: findom); ins; desf; eauto. specialize (H0 x); tauto. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms