proposition: Lemma H10_SU: H10 E -> SOU ag 2 (H10_to_SOU E).
proof: Proof. intros [sigma H]. exists []. exists (enc_sol sigma). split. now eapply typing_forward. intros s t; change s with (fst (s,t)) at 2; change t with (snd (s,t)) at 3. remember (s,t) as e. clear Heqe s t. intros H'; cbn in *. eapply in_Equations in H' as (d & ? & ?). destruct d; cbn in *; intuition idtac; subst. all: try eapply forward_add. all: try eapply forward_consts. all: try eapply forward_mul. all: try eapply forward_vars. all: try eapply enc_sol_encodes. all: eapply H in H0; inv H0; (eauto 2). apply enc_sol_T. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)