proposition: Lemma fof__fof1 : FunctionalChoice_on Tpoint tFOF -> forall F, FOF F -> exists F1, F <-> fof1_prop F1 .
proof: Proof. intros choice F HFOF. induction HFOF. - exists (eq_fof1 A B); intuition. - exists (bet_fof1 A B C); intuition. - exists (cong_fof1 A B C D); intuition. - destruct IHHFOF as [F1]. exists (not_fof1 F1). simpl; intuition. - destruct IHHFOF1 as [F1]; destruct IHHFOF2 as [F2]; exists (and_fof1 F1 F2); simpl; intuition. - destruct IHHFOF1 as [F1]; destruct IHHFOF2 as [F2]; exists (or_fof1 F1 F2); simpl; intuition. - destruct IHHFOF1 as [F1]; destruct IHHFOF2 as [F2]; exists (implies_fof1 F1 F2); simpl; intuition. - destruct (choice (fun A => (fun F1 => P A <-> fof1_prop F1)) H0) as [f]. exists (forall_fof1 f); simpl. split; intros HH A; apply H1, HH. - destruct (choice (fun A => (fun F1 => P A <-> fof1_prop F1)) H0) as [f]. exists (exists_fof1 f); simpl. split; intros [A HA]; exists A; apply H1, HA. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Definitions Logic.ChoiceFacts