proposition: Lemma countable_formulas: countable_set all_formulas.
proof: Proof. rewrite /all_formulas. move:(induction_defined_pr next_formulas atomic_formulas). rewrite -/formulas_rec; move => [h1 h2 h3 h4]. have ff:= proj1 h2. rewrite - (surjective_pr0 h2) (ImfE ff) -(setUb_alt(function_fgraph ff)). apply: countable_union. rewrite (domain_fg ff) h1; apply/countableP. rewrite - aleph0_pr1; exact: (cleR (CS_aleph0)). have ha: forall x y, countable_set (doubleton x y). move / (oclt3 CS1 CS_aleph0): olt_1omega => [H1 _]. move / (oclt3 CS2 CS_aleph0): olt_2omega => [H2 _]. move => x y; apply /countableP; case: (equal_or_not x y) => exy. by rewrite exy cardinal_set1. by rewrite (cardinal_set2 exy). have hb: countable_set variables by apply:countable_Nat. move => x; rewrite (domain_fg ff) h1 -/(Vf _ _). move:x; apply: Nat_induction. rewrite h3 /atomic_formulas; apply: countable_setX2; first by apply: ha. by apply: countable_setX2. move => n nN Hrec; rewrite (h4 _ nN);apply:countable_setU2. apply:countable_setU2. apply:countable_setU2 => //; apply:countable_setX2 => //; apply: ha. by apply:countable_setX2 => //; [apply: ha | apply:countable_setX2]. by apply:countable_setX2; [ apply: ha | apply:countable_setX2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)