proposition: Fact dp_inst_par_eval φ ν p : dp_eval φ ν (dp_inst_par p) = dp_eval φ σ p.
proof: Proof. induction p as [ | | | [] ]; simpl; f_equal; auto. Qed.
imports: List Arith Lia  Undecidability.Shared.Libs.DLW(utils_tac utils_list sums pos vec) Undecidability.H10.Dio(dio_logic dio_elem)