proposition: Lemma sub_sol_enc sigma x n: sigma x = enc n -> sub_sol sigma x = n.
proof: Proof. intros H; unfold sub_sol; destruct dec_enc as [[m H']|H']. rewrite H' in H; eapply enc_injective in H; trivial. eapply H' in H; intuition. 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