proposition: Lemma embed_env_eval n (p : dio_polynomial (Fin.t n) (Fin.t 0)) nu phi : dp_eval phi nu p = dp_eval_pfree (embed_env phi) (embed_poly p).
proof: Proof. induction p. - reflexivity. - cbn. unfold embed_env. destruct Compare_dec.lt_dec as [H|H]. + erewrite of_nat_ext, of_nat_to_nat_inv. reflexivity. + exfalso. apply H. apply proj2_sig. - inversion p. - cbn [dp_eval]. rewrite IHp1, IHp2. now destruct d. Qed.
imports: Undecidability.H10(H10 Dio.dio_single H10p) Undecidability.Synthetic.Definitions Fin