fact: Fixpoint dp_ren_par p : dio_polynomial V Q := match p with | dp_nat c => dp_nat c | dp_var v => dp_var v | dp_par p => dp_par (f p) | dp_comp o p q => dp_comp o (dp_ren_par p) (dp_ren_par q) end.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)