proposition: Lemma type_enum_t_fo_term : type_enum_t (fo_term (ar_syms Σ)).
proof: Proof. Proof using H3 H1. apply type_enum_t_by_measure with (m := @fo_term_height _ _). induction n as [ | n Hn ]. + generalize Hnat. apply opt_enum_t_image with in_var. intros [ i | s v ]; simpl. * split; auto; exists i; auto. * split; try lia; intros (? & _ & ?); discriminate. + generalize (opt_enum_t_dep_sum _ _ H1 H3 (fun s => opt_enum_t_vec (ar_syms Σ s) Hn)); intros H5. generalize (opt_enum_t_sum Hnat H5). apply opt_enum_t_image with (f := fun p => match p with | inl i => in_var i | inr (existT _ s v) => @in_fot _ _ s v end). intros t; split. * destruct t as [ i | s v ]; intros H. - exists (inl i); auto. - exists (inr (existT _ s v)); simpl; split; auto. intros p; generalize (fo_term_height_lt _ v p); lia. * intros ([ i | (s,v) ] & H); revert H; simpl. - intros (_ & ->); simpl; lia. - intros (G & ->); simpl; apply le_n_S, lmax_spec, Forall_forall. intros x Hx; apply vec_list_inv in Hx. destruct Hx as (p & Hp); revert Hp; rew vec; intros ->; auto. 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)