proposition: Fact fo_term_height_lt s v p : fo_term_height (vec_pos v p) < fo_term_height (@in_fot s v).
proof: Proof. simpl; apply le_n_S. generalize (in_vec_pos (vec_map fo_term_height v) p); rew vec. generalize (fo_term_height (vec_pos v p)) (vec_map fo_term_height v). clear v p; intros i v; rewrite in_vec_list. apply lmax_prop. Qed.
imports: List Arith Lia Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable fol_ops fo_sig)