fact: Fixpoint fof1_prop (F:tFOF) := match F with eq_fof1 A B => A = B | bet_fof1 A B C => Bet A B C | cong_fof1 A B C D => Cong A B C D | not_fof1 F1 => ~ fof1_prop F1 | and_fof1 F1 F2 => fof1_prop F1 /\ fof1_prop F2 | or_fof1 F1 F2 => fof1_prop F1 \/ fof1_prop F2 | implies_fof1 F1 F2 => fof1_prop F1 -> fof1_prop F2 | forall_fof1 P => forall A, fof1_prop (P A) | exists_fof1 P => exists A, fof1_prop (P A) end.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Definitions Logic.ChoiceFacts