proposition: Fact dp_eval_ext φ ν φ' ν' p : (forall v, In v (dp_var_list p) -> φ v = φ' v) -> (forall i, In i (dp_par_list p) -> ν i = ν' i) -> dp_eval φ ν p = dp_eval φ' ν' p.
proof: Proof. induction p as [ | | | [] p Hp q Hq ]; simpl; intros H1 H2; f_equal; auto; ((apply Hp || apply Hq); intros; [ apply H1 | apply H2 ]; apply in_or_app; auto). Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.H10.Dio(dio_logic dio_single) Undecidability.H10.ArithLibs(Zp lagrange)