proposition: Theorem type_enum_t_fol_form : type_enum_t (fol_form Σ).
proof: Proof. Proof using H4 H3 H2 H1. apply type_enum_t_by_measure with (m := @fol_height _). induction n as [ | n Hn ]. + exists (fun n => None). intros [ | | | ]; simpl; split; try lia; intros (? & ?); discriminate. + generalize type_enum_t_fo_term; intros H5. apply type_enum_opt_enum_t in H5. generalize (opt_enum_t_dep_sum _ _ H2 H4 (fun r => opt_enum_t_vec (ar_rels Σ r) H5)); intros H6. generalize (opt_enum_t_prod Hfol_bop (opt_enum_t_prod Hn Hn)); intros H7. generalize (opt_enum_t_prod Hfol_qop Hn); intros H8. generalize (opt_enum_t_sum (opt_enum_t_sum Hunit H6) (opt_enum_t_sum H7 H8)). apply opt_enum_t_image with (f := fun p => match p with | inl (inl _) => ⊥ | inl (inr (existT _ r v)) => fol_atom r v | inr (inl (b,(A,B))) => fol_bin b A B | inr (inr (q,A)) => fol_quant q A end). intros A; split. * revert A; intros [ | r v | b A B | q A ]; simpl; intros H. - exists (inl (inl tt)); auto. - exists (inl (inr (existT _ r v))); simpl; auto. - apply le_S_n in H. exists (inr (inl (b,(A,B)))); simpl; repeat split; auto; apply Nat.le_trans with (2 := H). ++ apply Nat.le_max_l. ++ apply Nat.le_max_r. - apply le_S_n in H. exists (inr (inr (q,A))); simpl; repeat split; auto. * intros ([ [ [] | (r&v) ] | [ (b,(B,C)) | (q,B) ] ] & H); revert H; simpl. - intros (_ & ->); simpl; lia. - intros (_ & ->); simpl; lia. - intros ((_ & G1 & G2) & ->); simpl. apply le_n_S, Nat.max_lub; auto. - intros ((_ & G1) & ->); simpl; lia. Qed.
imports: List Arith Lia Max Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable enumerable fol_ops fo_sig fo_terms fo_logic)