proposition: Lemma H10_DWK : H10 E -> SOU X 3 (H10_to_DWK X E).
proof: Proof. intros [theta H]. exists []. exists (encs theta). split. now eapply forward_typing. intros s t H'; cbn. change s with (fst (s, t)); change t with (snd (s, t)) at 2. remember (s,t) as q. clear Heqq. cbn in *. eapply in_Equations in H' as (e & ? & ?). eapply H in H0. destruct e; cbn in *; intuition idtac; subst. all: try eapply forward_add. all: try eapply forward_consts. all: try eapply forward_mult. all: try eapply forward_vars. all: unfold encs, funcomp; eauto. try eapply enc_sol_encodes. all: inv H0; eauto. Qed.
imports: List Arith Lia Undecidability.HOU(std.std calculus.calculus) Undecidability.HOU.second_order(diophantine_equations dowek.encoding) Undecidability.HOU.unification.nth_order_unification