fact: Definition dio_poly_pos m p : (forall x, In x (dp_var_list p) -> x < m) -> { q | forall φ ν, dp_eval φ ν p = dp_eval (vec_pos (fun2vec 0 m φ)) ν q }.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)