fact: Fixpoint dp_inst_par (p : dio_polynomial V P) : dio_polynomial V E := match p with | dp_nat c => dp_nat c | dp_var v => dp_var v | dp_par p => dp_nat (σ p) | dp_comp o p q => dp_comp o (dp_inst_par p) (dp_inst_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)