proposition: Lemma embed_spec x : H10 x <-> H10p (embed x).
proof: Proof. destruct x as (n & p & q). cbn. split; intros [phi H]; cbn in H. - exists (embed_env phi). cbn. now rewrite !embed_env_eval in H. - exists (cut_env phi). cbn. now rewrite !cut_env_eval. Qed.
imports: Undecidability.H10(H10 Dio.dio_single H10p) Undecidability.Synthetic.Definitions Fin