proposition: Lemma finite_dec_forall: forall (X:Type) (P:X->Prop), FiniteT X -> (forall x:X, P x \/ ~ P x) -> (forall x:X, P x) \/ (exists x:X, ~ P x).
proof: Proof. intros. revert P H0. induction H. - left. destruct x. - intros. case (IHFiniteT (fun x:T => P (Some x)) (fun x:T => H0 (Some x))). + intro. case (H0 None). * left. destruct x; auto. * right. exists None. assumption. + right. destruct H1 as [x]. exists (Some x). assumption. - intros. destruct H0. case (IHFiniteT (fun x:X => P (f x)) (fun x:X => H1 (f x))). + left. intro y. rewrite <- H2. apply H3. + right. destruct H3 as [x]. exists (f x). assumption. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)