proposition: Lemma cut_env_eval n (p : dio_polynomial (Fin.t n) (Fin.t 0)) nu phi : dp_eval (cut_env phi) nu p = dp_eval_pfree phi (embed_poly p).
proof: Proof. induction p. - reflexivity. - reflexivity. - inversion p. - cbn [dp_eval]. rewrite IHp1, IHp2. now destruct d. Qed.
imports: Undecidability.H10(H10 Dio.dio_single H10p) Undecidability.Synthetic.Definitions Fin