proposition: Fact dp_proj_par_eval φ ν p : dp_eval φ ν (dp_proj_par p) = dp_eval φ (fun i => match le_lt_dec n i with left _ => 0 | right H => ν (nat2pos H) end) p.
proof: Proof. induction p as [ | | p | [] ]; simpl; f_equal; auto. destruct (le_lt_dec n p); auto. Qed.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)