fact: Fixpoint dp_proj_par p : dio_polynomial V (pos n) := match p with | dp_nat c => dp_nat c | dp_var v => dp_var v | dp_par p => match le_lt_dec n p with left _ => dp_nat 0 | right H => dp_par (nat2pos H) end | dp_comp o p q => dp_comp o (dp_proj_par p) (dp_proj_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)